Types.v

Require Termes.
Require Conv.
Require Export MyList.

  Definition env := (list term).

  Definition item_lift := [t:term][e:env][n:nat]
     (Ex2 ([u:term]t=(lift (S n) u)) [u:term](item term u (e::(list term)) n)).

Section Typage.

  Mutual Inductive wf: env->Prop :=
    wf_nil: (wf (nil ?))
  | wf_var: (e:env)(T:term)(s:sort)(typ e T (Srt s))->(wf (cons ? T e))

  with typ: env->term->term->Prop :=
    type_prop: (e:env)(wf e)->(typ e (Srt prop) (Srt kind))
  | type_var: (e:env)(wf e)->(v:nat)(t:term)(item_lift t e v)
                   ->(typ e (Ref v) t)
  | type_abs: (e:env)(T:term)(s1:sort)(typ e T (Srt s1))
                  ->(M,U:term)(s2:sort)(typ (cons ? T e) U (Srt s2))
                    ->(typ (cons ? T e) M U)
                    ->(typ e (Abs T M) (Prod T U))
  | type_app: (e:env)(v,V:term)(typ e v V)
                ->(u,Ur:term)(typ e u (Prod V Ur))
                   ->(typ e (App u v) (subst v Ur))
  | type_prod: (e:env)(T:term)(s1:sort)(typ e T (Srt s1))
                   ->(U:term)(s2:sort)(typ (cons ? T e) U (Srt s2))
                     ->(typ e (Prod T U) (Srt s2))
  | type_conv: (e:env)(t,U,V:term)(typ e t U)->(conv U V)
        ->(s:sort)(typ e V (Srt s))->(typ e t V).

  Hint wf_nil type_prop type_var.

  Lemma typ_free_db: (e:env)(t,T:term)(typ e t T)
                          ->(free_db (length ? e) t).
(Induction 1; Intros; Auto).
Inversion_clear H1.
Apply db_ref.
(Elim H3; Simpl; Intros; Auto).
Save.

  Lemma typ_wf: (e:env)(t,T:term)(typ e t T)->(wf e).
Induction 1;Auto.
Save.

  Lemma wf_sort: (n:nat)(e,f:env)(trunc ? (S n) e f)->(wf e)
        ->(t:term)(item ? t e n)
         ->(Ex [s:sort](typ f t (Srt s))).
Induction n.
Do 3 Intro.
Inversion_clear H.
Inversion_clear H0.
Intros.
Inversion_clear H0.
Inversion_clear H.
Exists s;Auto.

Do 5 Intro.
Inversion_clear H0.
Intros.
Inversion_clear H2.
Inversion_clear H0.
Elim H with e0 f t ;Intros;Auto.
Exists x0;Auto.

Apply typ_wf with x (Srt s) ;Auto.
Save.

  Definition inv_type: Prop->env->term->term->Prop :=
    [P:Prop][e:env][t:term][T:term]Cases t of
       (Srt prop) => (conv T (Srt kind))->P
     | (Srt kind) => True
     | (Ref n) => (x:term)(item ? x e n)->(conv T (lift (S n) x))->P
     | (Abs A M) => (s1,s2:sort)(U:term)(typ e A (Srt s1))
                       ->(typ (cons ? A e) M U)
                        ->(typ (cons ? A e) U (Srt s2))->(conv T (Prod A U))->P
     | (App u v) => (Ur,V:term)(typ e v V)->(typ e u (Prod V Ur))
                  ->(conv T (subst v Ur))->P
     | (Prod A B) => (s1,s2:sort)(typ e A (Srt s1))
                       ->(typ (cons ? A e) B (Srt s2))
                        ->(conv T (Srt s2))->P
     end.

  Lemma inv_type_conv: (P:Prop)(e:env)(t,U,V:term)(conv U V)
      ->(inv_type P e t U)->(inv_type P e t V).
Do 6 Intro.
Cut (x:term)(conv V x)->(conv U x).
Intro.
Case t;Simpl;Intros.
Generalize H1 .
Elim s;Auto;Intros.

(Apply H1 with x ;Auto).

(Apply H1 with s1 s2 U0 ;Auto).

(Apply H1 with Ur V0 ;Auto).

(Apply H1 with s1 s2 ;Auto).

Intros.
(Apply trans_conv_conv with V ;Auto).
Save.

  Theorem typ_inversion: (P:Prop)(e:env)(t,T:term)(typ e t T)
                          ->(inv_type P e t T)
                           ->P.
Induction 1;Simpl;Intros.
Auto.

Elim H1;Intros.
Apply H2 with x ;Auto.
Rewrite -> H3;Auto.

Apply H6 with s1 s2 U ;Auto.

Apply H4 with Ur V ;Auto.

Apply H4 with s1 s2 ;Auto.

Apply H1.
(Apply inv_type_conv with V ;Auto).
Save.

  Lemma inv_typ_kind: (e:env)(t:term)~(typ e (Srt kind) t).
(Red;Intros).
(Apply typ_inversion with e (Srt kind) t ;Simpl;Auto).
Save.

  Lemma inv_typ_prop: (e:env)(T:term)(typ e (Srt prop) T)->(conv T (Srt kind)).
Intros.
(Apply typ_inversion with e (Srt prop) T ;Simpl;Auto).
Save.

  Lemma inv_typ_ref: (P:Prop)(e:env)(T:term)(n:nat)(typ e (Ref n) T)
    ->((U:term)(item ? U e n)->(conv T (lift (S n) U))->P)
     ->P.
Intros.
(Apply typ_inversion with e (Ref n) T ;Simpl;Intros;Auto).
(Apply H0 with x ;Auto).
Save.

  Lemma inv_typ_abs: (P:Prop)(e:env)(A,M,U:term)(typ e (Abs A M) U)->
            ((s1,s2:sort)(T:term)(typ e A (Srt s1))->(typ (cons ? A e) M T)
                    ->(typ (cons ? A e) T (Srt s2))->(conv (Prod A T) U)->P)
             ->P.
Intros.
(Apply typ_inversion with e (Abs A M) U ;Simpl;Auto;Intros).
(Apply H0 with s1 s2 U0 ;Auto).
Save.

  Lemma inv_typ_app: (P:Prop)(e:env)(u,v,T:term)(typ e (App u v) T)->
      ((V,Ur:term)(typ e u (Prod V Ur))->(typ e v V)
          ->(conv T (subst v Ur))->P)
       ->P.
Intros.
(Apply typ_inversion with e (App u v) T ;Simpl;Auto;Intros).
(Apply H0 with V Ur ;Auto).
Save.

  Lemma inv_typ_prod: (P:Prop)(e:env)(T,U,s:term)(typ e (Prod T U) s)->
       ((s1,s2:sort)(typ e T (Srt s1))->(typ (cons ? T e) U (Srt s2))
                      ->(conv (Srt s2) s)->P)
         ->P.
Intros.
(Apply typ_inversion with e (Prod T U) s ;Simpl;Auto;Intros).
(Apply H0 with s1 s2 ;Auto).
Save.

  Lemma typ_mem_kind: (e:env)(t,T:term)(mem_sort kind t)->~(typ e t T).
Red;Intros.
Apply typ_inversion with e t T ;Auto.
Generalize e T .
Clear H0.
Elim H;Simpl;Auto;Intros.
Apply typ_inversion with e0 u (Srt s1) ;Auto.

Apply typ_inversion with (cons term u e0) v (Srt s2) ;Auto.

Apply typ_inversion with e0 u (Srt s1) ;Auto.

Apply typ_inversion with (cons term u e0) v U ;Auto.

Apply typ_inversion with e0 u (Prod V Ur) ;Auto.

Apply typ_inversion with e0 v V ;Auto.
Save.

  Lemma inv_typ_conv_kind: (e:env)(t,T:term)(conv t (Srt kind))->~(typ e t T).
Intros.
Apply typ_mem_kind.
Apply red_sort_mem.
(Elim church_rosser with t (Srt kind) ;Intros;Auto).
(Rewrite -> (red_normal (Srt kind) x);Auto).
(Red;Red;Intros).
Inversion_clear H2.
Save.

  Inductive ins_in_env [A:term]: nat->env->env->Prop :=
     ins_O: (e:env)(ins_in_env A O e (cons ? A e))
   | ins_S: (n:nat)(e,f:env)(t:term)(ins_in_env A n e f)
    ->(ins_in_env A (S n) (cons ? t e) (cons ? (lift_rec (S O) t n) f)).

  Hint ins_O ins_S.

  Lemma ins_item_ge: (A:term)(n:nat)(e,f:env)(ins_in_env A n e f)
           ->(v:nat)(le n v)
                      ->(t:term)(item ? t e v)->(item ? t f (S v)).
Induction 1;Auto.
Destruct v;Intros.
Inversion_clear H2.

(Inversion_clear H3;Auto).
Save.

  Lemma ins_item_lt: (A:term)(n:nat)(e,f:env)(ins_in_env A n e f)
           ->(v:nat)(gt n v)
            ->(t:term)(item_lift t e v)->(item_lift (lift_rec (S O) t n) f v).
Induction 1.
Intros.
Inversion_clear H0.

Destruct v;Intros.
Elim H3;Intros.
Rewrite -> H4.
Exists (lift_rec (S O) t n0) ;Auto.
Inversion_clear H5.
Elim permute_lift with t n0 ;Auto.

Elim H3;Intros.
Rewrite -> H4.
Inversion_clear H5.
Elim H1 with n1 (lift (S n1) x) ;Intros;Auto.
Exists x0 ;Auto.
Pattern 1 (lift (S (S n1)) x0) .
(Rewrite -> simpl_lift;Auto).
Elim H5.
Change (eq ? (lift_rec (S O) (lift (S (S n1)) x) (S n0))
         (lift (S O) (lift_rec (S O) (lift (S n1) x) n0))).
Rewrite -> (permute_lift (lift (S n1) x) n0).
Unfold 2 lift .
Pattern (lift (S (S n1)) x) .
(Rewrite -> simpl_lift;Auto).

Exists x ;Auto.
Save.

  Lemma typ_weak_weak: (A:term)(e:env)(t,T:term)(typ e t T)
                         ->(n:nat)(f:env)(ins_in_env A n e f)
                           ->(wf f)
                       ->(typ f (lift_rec (S O) t n) (lift_rec (S O) T n)).
(Induction 1; Simpl; Intros; Auto).
(Elim (le_gt_dec n v); Intros; Apply type_var; Auto).
(Elim H1; Intros).
Exists x.
Rewrite -> H4.
Unfold lift.
(Rewrite -> simpl_lift_rec; Simpl; Auto).

(Apply ins_item_ge with A n e0; Auto).

(Apply ins_item_lt with A e0; Auto).

Cut (wf (cons ? (lift_rec (S O) T0 n) f)).
Intro.
(Apply type_abs with s1 s2; Auto).

(Apply wf_var with s1; Auto).

Rewrite -> distr_lift_subst.
(Apply type_app with (lift_rec (S O) V n); Auto).

Cut (wf (cons ? (lift_rec (S O) T0 n) f)).
Intro.
(Apply type_prod with s1; Auto).

(Apply wf_var with s1; Auto).

(Apply type_conv with (lift_rec (S O) U n) s; Auto).
Save.

  Theorem thinning: (e:env)(t,T:term)(typ e t T)
                ->(A:term)(wf (cons ? A e))
                 ->(typ (cons ? A e) (lift (S O) t) (lift (S O) T)).
Unfold lift.
Intros.
Inversion_clear H0.
(Apply typ_weak_weak with A e; Auto).
(Apply wf_var with s; Auto).
Save.

  Lemma thinning_n: (n:nat)(e,f:env)(trunc ? n e f)->(t,T:term)(typ f t T)
                      ->(wf e)->(typ e (lift n t) (lift n T)).
Induction n.
Intros.
Rewrite -> lift0.
Rewrite -> lift0.
(Replace e with f;Auto).
(Inversion_clear H;Auto).

Do 8 Intro.
Inversion_clear H0.
Intro.
Rewrite -> simpl_lift;Auto.
Pattern (lift (S n0) T) .
Rewrite -> simpl_lift;Auto.
Inversion_clear H0.
Change (typ (cons ? x e0) (lift (S O) (lift n0 t))
         (lift (S O) (lift n0 T))).
Apply thinning;Auto.
(Apply H with f ;Auto).
Apply typ_wf with x (Srt s) ;Auto.

Apply wf_var with s ;Auto.
Save.

  Lemma wf_sort_lift: (n:nat)(e:env)(t:term)(wf e)->(item_lift t e n)
         ->(Ex [s:sort](typ e t (Srt s))).
Induction n.
(Destruct e;Intros).
(Elim H0;Intros).
Inversion_clear H2.

(Elim H0;Intros).
Rewrite -> H1.
Inversion_clear H2.
Inversion_clear H.
Exists s.
(Replace (Srt s) with (lift (S O) (Srt s));Auto).
(Apply thinning;Auto).
(Apply wf_var with s ;Auto).

Intros.
(Elim H1;Intros).
Rewrite -> H2.
Generalize H0 .
(Inversion_clear H3;Intros).
Rewrite simpl_lift;Auto.
(Cut (wf l);Intros).
Elim H with l (lift (S n0) x) ;Intros;Auto.
Inversion_clear H3.
Exists x0.
Change (typ (cons ? y l) (lift (S O) (lift (S n0) x)) (lift (S O) (Srt x0))).
(Apply thinning;Auto).
(Apply wf_var with s ;Auto).

(Exists x;Auto).

Inversion_clear H3.
(Apply typ_wf with y (Srt s) ;Auto).
Save.

  Inductive sub_in_env [t,T:term]: nat->env->env->Prop :=
     sub_O: (e:env)(sub_in_env t T O (cons ? T e) e)
   | sub_S: (e,f:env)(n:nat)(u:term)(sub_in_env t T n e f)
         ->(sub_in_env t T (S n) (cons ? u e) (cons ? (subst_rec t u n) f)).

  Hint sub_O sub_S.

  Lemma nth_sub_sup: (t,T:term)(n:nat)(e,f:env)(sub_in_env t T n e f)
           ->(v:nat)(le n v)
                      ->(u:term)(item ? u e (S v))->(item ? u f v).
Induction 1.
Intros.
(Inversion_clear H1;Auto).

Destruct v;Intros.
Inversion_clear H2.

(Inversion_clear H3;Auto).
Save.

  Lemma nth_sub_eq: (t,T:term)(n:nat)(e,f:env)(sub_in_env t T n e f)
                        ->(item ? T e n).
(Induction 1;Auto).
Save.

  Lemma nth_sub_inf: (t,T:term)(n:nat)(e,f:env)(sub_in_env t T n e f)
           ->(v:nat)(gt n v)
            ->(u:term)(item_lift u e v)->(item_lift (subst_rec t u n) f v).
Induction 1.
Intros.
Inversion_clear H0.

Destruct v;Intros.
Elim H3;Intros.
Rewrite -> H4.
Inversion_clear H5.
Exists (subst_rec t u n0) ;Auto.
(Apply commut_lift_subst;Auto).

Elim H3;Intros.
Rewrite -> H4.
Inversion_clear H5.
Elim H1 with n1 (lift (S n1) x) ;Intros;Auto.
Exists x0 ;Auto.
(Rewrite -> simpl_lift;Auto).
Pattern (lift (S (S n1)) x0) .
(Rewrite -> simpl_lift;Auto).
Elim H5.
Change (eq ? (subst_rec t (lift (S O) (lift (S n1) x)) (S n0))
         (lift (S O) (subst_rec t (lift (S n1) x) n0))).
(Apply commut_lift_subst;Auto).

Exists x ;Auto.
Save.

  Lemma typ_sub_weak: (g:env)(d:term)(t:term)(typ g d t)
                       ->(e:env)(u,U:term)(typ e u U)
                        ->(f:env)(n:nat)(sub_in_env d t n e f)
                         ->(wf f)
                          ->(trunc ? n f g)
                    ->(typ f (subst_rec d u n) (subst_rec d U n)).
(Induction 2;Simpl;Intros;Auto).
(Elim (lt_eq_lt_dec n v);Intros).
Elim H2.
Elim y.
(Case v;Intros).
Inversion_clear y0.

Simpl.
Rewrite -> H6.
(Rewrite -> simpl_subst;Auto).
(Apply type_var;Auto).
(Exists x ;Auto).
(Apply nth_sub_sup with d t n e0 ;Auto).

Intros.
Rewrite -> H6.
Elim y0.
(Rewrite -> simpl_subst;Auto).
Replace x with t.
Apply thinning_n with g ;Auto.

Apply fun_item with e0 v ;Auto.
Apply nth_sub_eq with d f ;Auto.
Elim y0;Auto.

Apply type_var;Auto.
Apply nth_sub_inf with t e0 ;Auto.

Cut (wf (cons ? (subst_rec d T n) f));Intros.
Apply type_abs with s1 s2 ;Auto.

Apply wf_var with s1 ;Auto.

Rewrite -> distr_subst.
Apply type_app with (subst_rec d V n) ;Auto.

Cut (wf (cons ? (subst_rec d T n) f));Intros.
Apply type_prod with s1 ;Auto.

Apply wf_var with s1 ;Auto.

Apply type_conv with (subst_rec d U0 n) s ;Auto.
Save.

  Theorem substitution: (e:env)(t,u,U:term)(typ (cons ? t e) u U)
              ->(d:term)(typ e d t)
                ->(typ e (subst d u) (subst d U)).
Intros.
Unfold subst .
Apply typ_sub_weak with e t (cons ? t e) ;Auto.
(Apply typ_wf with d t ;Auto).
Save.

  Theorem typ_unique: (e:env)(t,T:term)(typ e t T)->(U:term)(typ e t U)
                            ->(conv T U).
Induction 1;Intros.
Apply sym_conv.
(Apply inv_typ_prop with e0 ;Auto).

(Apply inv_typ_ref with e0 U v ;Auto;Intros).
(Elim H1;Intros).
Rewrite -> H5.
(Elim fun_item with term U0 x e0 v ;Auto).

Apply inv_typ_abs with e0 T0 M U0 ;Auto;Intros.
Apply trans_conv_conv with (Prod T0 T1) ;Auto.

Apply inv_typ_app with e0 u v U ;Auto;Intros.
Apply trans_conv_conv with (subst v Ur0) ;Auto.
(Unfold subst ;Apply conv_conv_subst;Auto).
Apply inv_conv_prod_r with V V0 ;Auto.

(Apply inv_typ_prod with e0 T0 U U0 ;Auto;Intros).
(Apply trans_conv_conv with (Srt s3) ;Auto).

(Apply trans_conv_conv with U ;Auto).
Save.

  Theorem type_case: (e:env)(t,T:term)(typ e t T)->
                  (Ex [s:sort](typ e T (Srt s)))\/(T=(Srt kind)).
Induction 1;Intros;Auto.
Left.
(Elim wf_sort_lift with v e0 t0 ;Auto;Intros).
(Exists x;Auto).

Left.
Exists s2.
(Apply type_prod with s1 ;Auto).

Left.
(Elim H3;Intros).
(Elim H4;Intros).
(Apply inv_typ_prod with e0 V Ur (Srt x) ;Auto;Intros).
Exists s2.
(Replace (Srt s2) with (subst v (Srt s2));Auto).
Apply substitution with V ;Auto.

Discriminate H4.

(Case s2;Auto).
Left.
Exists kind.
Apply type_prop.
(Apply typ_wf with T0 (Srt s1) ;Auto).

Left.
(Exists s;Auto).
Save.

  Lemma type_kind_not_conv: (e:env)(t,T:term)(typ e t T)->(typ e t (Srt kind))
                           ->(T=(Srt kind)).
Intros.
Elim type_case with e t T ;Intros;Auto.
(Elim H1;Intros).
(Elim inv_typ_conv_kind with e T (Srt x) ;Auto).
(Apply typ_unique with e t ;Auto).
Save.

  Lemma type_free_db: (e:env)(t,T:term)(typ e t T)
                          ->(free_db (length ? e) T).
Intros.
(Elim type_case with e t T; Intros; Auto).
Inversion_clear H0.
(Apply typ_free_db with (Srt x); Auto).

(Rewrite -> H0; Auto).
Save.

  Inductive red1_in_env: env->env->Prop :=
     red1_env_hd: (e:env)(t,u:term)(red1 t u)
                    ->(red1_in_env (cons ? t e) (cons ? u e))
   | red1_env_tl: (e,f:env)(t:term)(red1_in_env e f)
                     ->(red1_in_env (cons ? t e) (cons ? t f)).

  Hint red1_env_hd red1_env_tl.

  Lemma red_item: (n:nat)(t:term)(e:env)(item_lift t e n)
      ->(f:env)(red1_in_env e f)
       ->(item_lift t f n)
          \/( ((g:env)((trunc ? (S n) e g)->(trunc ? (S n) f g)))
              /\ (Ex2 [u:term](red1 t u) [u:term](item_lift u f n)) ).
Induction n.
Do 3 Intro.
Elim H.
Do 4 Intro.
Rewrite -> H0.
Inversion_clear H1.
Intros.
Inversion_clear H1.
Right.
Split;Intros.
Inversion_clear H1;Auto.

Exists (lift (S O) u) .
(Unfold lift ;Auto).

Exists u ;Auto.

Left.
Exists x ;Auto.

Do 5 Intro.
Elim H0.
Do 4 Intro.
Rewrite -> H1.
Inversion_clear H2.
Intros.
Inversion_clear H2.
Left.
Exists x ;Auto.

Elim H with (lift (S n0) x) l f0 ;Auto;Intros.
Left.
Elim H2;Intros.
Exists x0 ;Auto.
Rewrite -> simpl_lift.
Pattern (lift (S (S n0)) x0) .
Rewrite -> simpl_lift.
Elim H5;Auto.

Right.
Elim H2.
Induction 2;Intros.
Split;Intros.
Inversion_clear H9;Auto.

Elim H8;Intros.
Exists (lift (S (S n0)) x1) .
Rewrite -> simpl_lift.
Pattern (lift (S (S n0)) x1) .
Rewrite -> simpl_lift.
(Elim H9;Unfold 1 3 lift ;Auto).

Exists x1 ;Auto.

Exists x ;Auto.
Save.

  Lemma typ_red_env: (e:env)(t,T:term)(typ e t T)
                        ->(f:env)(red1_in_env e f)
                          ->(wf f)->(typ f t T).
(Induction 1; Intros).
Auto.

(Elim red_item with v t0 e0 f; Auto; Intros).
Inversion_clear H4.
Inversion_clear H6.
(Elim H1; Intros).
(Elim item_trunc with term v e0 x0; Intros; Auto).
(Elim wf_sort with v e0 x1 x0; Auto).
Intros.
(Apply type_conv with x x2; Auto).
Rewrite -> H6.
(Replace (Srt x2) with (lift (S v) (Srt x2)); Auto).
(Apply thinning_n with x1; Auto).

(Cut (wf (cons ? T0 f)); Intros).
(Apply type_abs with s1 s2; Auto).

(Apply wf_var with s1; Auto).

(Apply type_app with V; Auto).

(Cut (wf (cons ? T0 f)); Intros).
(Apply type_prod with s1; Auto).

(Apply wf_var with s1; Auto).

(Apply type_conv with U s; Auto).
Save.

  Lemma subj_red: (e:env)(t,T:term)(typ e t T)->
                     (u:term)(red1 t u)->(typ e u T).
(Induction 1; Intros).
Inversion_clear H1.

Inversion_clear H2.

Inversion_clear H6.
(Cut (wf (cons ? M' e0)); Intros).
(Apply type_conv with (Prod M' U) s2; Auto).
(Apply type_abs with s1 s2; Auto).
(Apply typ_red_env with (cons ? T0 e0); Auto).

(Apply typ_red_env with (cons ? T0 e0); Auto).

(Apply type_prod with s1; Auto).

(Apply wf_var with s1; Auto).

(Apply type_abs with s1 s2; Auto).

(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
Inversion_clear H5.
(Apply inv_typ_prod with e0 V Ur (Srt x); Intros; Auto).
Generalize H2 H3 .
Clear H2 H3.
(Inversion_clear H4; Intros).
(Apply inv_typ_abs with e0 T0 M (Prod V Ur); Intros; Auto).
(Apply type_conv with (subst v T1) s2; Auto).
(Apply substitution with T0; Auto).
(Apply type_conv with V s0; Auto).
(Apply inv_conv_prod_l with Ur T1; Auto).

Unfold subst.
(Apply conv_conv_subst; Auto).
(Apply inv_conv_prod_r with T0 V; Auto).

(Replace (Srt s2) with (subst v (Srt s2)); Auto).
(Apply substitution with V; Auto).

(Apply type_app with V; Auto).

(Apply type_conv with (subst N2 Ur) s2; Auto).
(Apply type_app with V; Auto).

Unfold subst.
(Apply conv_conv_subst; Auto).

(Replace (Srt s2) with (subst v (Srt s2)); Auto).
(Apply substitution with V; Auto).

Discriminate H5.

Inversion_clear H4.
(Apply type_prod with s1; Auto).
(Apply typ_red_env with (cons ? T0 e0); Auto).
(Apply wf_var with s1; Auto).

(Apply type_prod with s1; Auto).

(Apply type_conv with U s; Auto).
Save.

  Theorem subject_reduction: (e:env)(t,u:term)(red t u)
            ->(T:term)(typ e t T)->(typ e u T).
(Induction 1;Intros;Auto).
Apply subj_red with P ;Intros;Auto.
Save.

  Lemma type_reduction: (e:env)(t,T,U:term)(red T U)
                               ->(typ e t T)->(typ e t U).
Intros.
(Elim type_case with e t T; Intros; Auto).
Inversion_clear H1.
(Apply type_conv with T x; Auto).
(Apply subject_reduction with T; Auto).

(Elim red_normal with T U; Auto).
Rewrite -> H1.
(Red; Red; Intros).
Inversion_clear H2.
Save.

  Lemma typ_conv_conv:(e:env)(u,U,v,V:term)(typ e u U)->(typ e v V)->(conv u v)
                   ->(conv U V).
Intros.
(Elim church_rosser with u v ;Auto;Intros).
Apply typ_unique with e x .
Apply subject_reduction with u ;Auto.

Apply subject_reduction with v ;Auto.
Save.

End Typage.

  Hint ins_O ins_S.
  Hint sub_O sub_S.
  Hint red1_env_hd red1_env_tl.

31/03/97, 21:45