The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

It seems that you need Streicher's axiom K in order to achieve this. It 
has been proved for decidable types in the standard library Eqdep_dec 
for types with decidable equality.
The script below contains a proof of the uniquenes of derivations in 
your modelisation of lambda calculus under the hypothesis that equality 
is decidable on variables and function symbols.
Still I wonder if there's a simpler way to do it.

Require Import List.
Require Import Eqdep_dec.
Set Implicit Arguments.

Variable BaseType : Set.
Implicit Types a b c : BaseType.
Hypothesis eq_dec_BaseType : forall a b, {a=b} + {a<>b}.

Inductive SimpleType : Set :=
| BasicType(T: BaseType)
| ArrowType(A B : SimpleType).
Notation "x --> y" := (ArrowType x y) (at level 55, right 
associativity) : type_scope.
Notation "# x " := (BasicType x) (at level 0) : type_scope.
Implicit Types A B C : SimpleType.

Lemma eq_dec_SimpleType : forall A B, {A = B} + {A <> B}.
decide equality.
apply eq_dec_BaseType.
Qed.

Variable FunctionSymbol : Set.
Implicit Types f g h : FunctionSymbol.
Hypothesis eq_dec_FunctionSymbol : forall (f g: FunctionSymbol), {f=g} 
+ {f<>g}.

Variable f_type: FunctionSymbol -> SimpleType.

Definition Env := list (option SimpleType).

Definition EmptyEnv : Env := nil.
Implicit Type x y : nat.
Implicit Type E : Env.

Definition VarD  E x A := nth_error E x = Some (Some A).
Notation "E |= x := A" := (VarD E x A) (at level 60).

Lemma VarD_unique : forall E x A (v1 v2 : VarD E x A), v1 = v2.
unfold VarD; intros; generalize v1 v2; rewrite v1.
intros; apply K_dec_set; [idtac |  pattern v0; apply K_dec_set]; auto;
  decide equality; generalize a o; decide equality; apply 
eq_dec_SimpleType.
Qed.

Definition VarUD E x := nth_error E x = None \/ nth_error E x = Some 
None.
Notation "E |= x :!" := (VarUD E x) (at level 60).

Definition decl A E := Some A::E.
Definition declDummy E := None::E.

Inductive Preterm : Set :=
| Var(x: nat)
| Fun(f: FunctionSymbol)
| Abs(A: SimpleType)(M: Preterm)
| App(M N: Preterm).

Implicit Type Pt : Preterm.
Notation "^ f" := (Fun f) (at level 20).
Notation "% x" := (Var x) (at level 20).
Infix "@@" := App (at level 25, left associativity).
Notation "s [ x ]" := (s @@ x) (at level 30).
Notation "s [ x , y ]" := (s @@ x @@ y) (at level 30).
Notation " A ==> M" := (Abs A M) (at level 35).
Reserved Notation "E |- Pt := A" (at level 60).

Inductive Typing : Env -> Preterm -> SimpleType -> Set :=
| TVar: forall E x A, (E |= x := A) -> (E |- %x := A)
| TFun: forall E f,  (E |- ^f := f_type f)
| TAbs: forall E A B Pt, (decl A E |- Pt := B) -> (E |- A ==> Pt := A 
--> B)
| TApp: forall E A B Pt0 Pt1,
(E |- Pt0 := A --> B) ->
(E |- Pt1 := A) ->
(E |- Pt0 @@ Pt1 := B)
where "E |- Pt := A" := (Typing E Pt A).

Record Term : Set := buildT {
  env: Env;
  term: Preterm;
  type: SimpleType;
  typing: Typing env term type
}.

Implicit Types M N : Term.

Lemma eq_dec_Preterm : forall (a b : Preterm), {a = b} + {a <> b}.
decide equality.
generalize x x0; decide equality.
generalize f f0; apply eq_dec_FunctionSymbol.
generalize A A0; apply eq_dec_SimpleType.
Qed.

Lemma eq_dec_Env : forall (a b : Env), {a = b} + {a <> b}.
decide equality; generalize a o; decide equality; apply 
eq_dec_SimpleType.
Qed.

Lemma eq_dec_EPS : forall (a b : Env * Preterm * SimpleType), {a = b} + 
{a <> b}.
decide equality.
  apply eq_dec_SimpleType.
  generalize a p; decide equality.
    apply eq_dec_Preterm.
    apply eq_dec_Env.
Qed.

Lemma Type_unique : forall t e T1 T2 (d1 : Typing e t T1) (d2 : Typing 
e t T2), T1=T2.
induction t; intros; inversion d1; inversion d2; trivial.

  unfold  VarD in *.
  assert(Some (Some T1) = Some (Some T2)).
    transitivity (nth_error e x); auto.
  injection H7; trivial.

  rewrite(@IHt _ _ _ H3 H8); auto.

  set(e0 := IHt1 _ _ _ H2 H8); injection e0; auto.
Qed.

Lemma Deriv_unique : forall e t T (d1 d2 : Typing e t T), d1=d2.
refine(
  fix Deriv_unique e t T (d1 d2 : Typing e t T) {struct d1 } : d1 = d2 
:=
    match d1 as d1' in Typing e1 t1 T1, d2 as d2' in Typing e2 t2 T2 
return
      forall (cast : (e1,t1,T1) = (e2,t2,T2)), (e1,t1,T1) = (e,t,T) ->
        eq_rect (e1,t1,T1) (fun etT => match etT with (e,t,T) => Typing 
e t T end) d1' _ cast = d2'
    with
    | TVar _ _ _ _, TVar _ _ _ _ => _
    | TFun _ _, TFun _ _ => _
    | TAbs _ _ _ _ _, TAbs _ _ _ _ _ => _
    | TApp _ _ _ _ _ _ _, TApp _ _ _ _ _ _ _ => _
    | _, _ => _
    end (refl_equal _) (refl_equal _));
intros; destruct t; try discriminate;
try discriminate cast; try discriminate dis;
injection cast; intros; generalize cast; clear cast.

  generalize v v0; clear v v0.
  rewrite H0; rewrite H1; rewrite H2.
  intros; pattern cast; apply (K_dec_set eq_dec_EPS).
  rewrite (VarD_unique v v0); apply refl_equal.

  rewrite H1; rewrite H2.
  intros; pattern cast; apply (K_dec_set eq_dec_EPS); apply refl_equal.

  generalize t1; clear t1.
  rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H4.
  intros; pattern cast; apply (K_dec_set eq_dec_EPS).
  rewrite(Deriv_unique _ _ _ t0 t1); apply refl_equal.

  generalize t2 t3; clear t2 t3.
  rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H3.
  intros t2 t3.
  intros; pattern cast; apply (K_dec_set eq_dec_EPS).
  set(e0 := Type_unique t0 t2); injection e0; intro H7.
  generalize t2 t3; clear e0 t2 t3; rewrite <- H7.
  intros; rewrite(Deriv_unique _ _ _ t0 t2); rewrite(Deriv_unique _ _ _ 
t1 t3);
  apply refl_equal.
Qed.

Theorem deriv_uniq: forall M N, env M = env N -> term M = term N -> 
type M = type N -> M = N.
intros; destruct M; destruct N; simpl in *.
generalize typing0; clear typing0.
rewrite H; rewrite H0; rewrite H1.
intros.
rewrite(Deriv_unique typing0 typing1).
apply refl_equal.
Qed.

Lemma typing_uniq: forall M N, env M = env N -> term M = term N -> type 
M = type N.
intros; destruct M; destruct N; simpl in *.
generalize typing0; clear typing0.
rewrite H; rewrite H0; intros.
apply (Type_unique typing0 typing1).
Qed.

Lemma term_eq: forall M N, env M = env N -> term M = term N -> M = N.
intros; apply deriv_uniq; auto.
apply typing_uniq; auto.
Qed.