Class.v
Require Termes.
Require Conv.
Require Types.
Require Export MyLogicType.
(* Kind skeletons *)
Inductive
skel: Type :=
PROP: skel
| PROD: skel -> skel -> skel.
Lemma
EQ_skel: (a,b:skel)(ORT (a===b) (notT (a===b))).
(Induction a; Destruct b; Intros).
(Left; Auto).
(Right; Red; Intros).
Inversion X.
(Right; Red; Intros).
Inversion X1.
(Elim X with s1; Intros).
Elim y.
(Elim X0 with s2; Intros).
Elim y0.
(Left; Auto).
(Right; Red; Intros; Apply y0).
(Injection X1; Auto).
(Right; Red; Intros; Apply y).
(Injection X1; Auto).
Save.
(* Classes *)
Inductive
class: Type :=
Trm: class
| Typ: skel -> class
| Knd: skel -> class.
Definition
cls:= (TList class).
Definition
cv_skel: class->skel :=
[c:class]Cases c of
(Knd s) => s
| _ => PROP
end.
Definition
typ_skel: class->skel :=
[c:class]Cases c of
(Typ s) => s
| _ => PROP
end.
Lemma
commut_case: (A,B:Type)(f:A->B)(c:class)(bt:A)(bT,bK:skel->A)
(f (Case c of bt bT bK end))
== (Cases c of
Trm => (f bt)
| (Typ _) => (f (bT (typ_skel c)))
| (Knd _) => (f (bK (cv_skel c)))
end).
(Destruct c; Auto).
Save.
Fixpoint
cl_term [t:term]: cls->class :=
[i:cls]Cases t of
(Srt _) => (Knd PROP)
| (Ref n) => Cases (Tnth_def ? Trm i n) of
(Knd s) => (Typ s)
| _ => Trm
end
| (Abs A B) => ([j:cls]Cases (cl_term B j) (cl_term A i) of
(Typ s2) (Knd s1) => (Typ (PROD s1 s2))
| (Typ s) _ => (Typ s)
| (Knd _) _ => (Knd PROP)
| Trm _ => Trm
end (TCs ? (cl_term A i) i))
| (App u v) => Cases (cl_term u i) (cl_term v i) of
(Typ (PROD s1 s2)) (Typ s) => (Typ s2)
| (Typ s) _ => (Typ s)
| (Knd _) _ => (Knd PROP)
| Trm _ => Trm
end
| (Prod T U) => ([j:cls]Cases (cl_term U j) (cl_term T i) of
(Knd s2) (Knd s1) => (Knd (PROD s1 s2))
| (Knd s) _ => (Knd s)
| (Typ s) _ => (Typ s)
| c1 _ => c1
end (TCs ? (cl_term T i) i))
end.
Fixpoint
class_env [e:env]: cls :=
Cases e of
nil =>(TNl ?)
| (cons t f) => (TCs ? (cl_term t (class_env f)) (class_env f))
end.
Lemma
nth_class_env: (t:term)(e,f:env)(n:nat)(item ? t e n)
->(trunc ? (S n) e f)
->(cl_term t (class_env f))==(Tnth_def ? Trm (class_env e) n).
(Induction 1; Simpl; Intros).
Inversion_clear H0.
(Inversion_clear H1; Auto).
Apply H1.
(Inversion_clear H2; Auto).
Save.
Lemma
cl_term_lift: (x:class)(t:term)(k:nat)(f,g:cls)(TIns ? x k f g)
->(cl_term t f)==(cl_term (lift_rec (S O) t k) g).
(Induction t; Intros).
(Simpl; Auto).
Simpl.
(Elim (le_gt_dec k n); Simpl; Intros).
(Elim Tins_le with class k f g Trm x n; Auto).
(Elim Tins_gt with class k f g Trm x n; Auto).
Simpl.
(Elim H with k f g; Auto).
(Elim H0 with (S k) (TCs class (cl_term t0 f) f) (TCs class
(cl_term t0 f) g);
Auto).
(Simpl; Auto).
(Elim H with k f g; Auto).
(Elim H0 with k f g; Auto).
Simpl.
(Elim H with k f g; Auto).
(Elim H0 with (S k) (TCs class (cl_term t0 f) f) (TCs class
(cl_term t0 f) g);
Auto).
Save.
Lemma
class_env_trunc: (k:nat)(e,f:env)(trunc ? k e f)
-> (TTrunc ? k (class_env e) (class_env f)).
(Induction 1;Simpl; Auto).
Save.
Hint class_env_trunc.
Lemma
cl_trunc: (n:nat)(e,f:cls)(TTrunc ? n e f)
->(t:term)(cl_term (lift n t) e)==(cl_term t f).
(Induction 1; Intros).
(Rewrite -> lift0; Auto).
Elim H1.
Rewrite -> simpl_lift.
Unfold 1 lift.
Simpl.
(Elim cl_term_lift with x (lift k t) O e0 (TCs ? x e0); Auto).
Save.
(* Loose stability results *)
Inductive
loose_eqc: class->class->Prop :=
leqc_trm: (loose_eqc Trm Trm)
| leqc_typ: (s1,s2:skel)(loose_eqc (Typ s1) (Typ s2))
| leqc_ord: (s:skel)(loose_eqc (Knd s) (Knd s)).
Hint leqc_trm leqc_typ leqc_ord.
Lemma
refl_loose_eqc: (c:class)(loose_eqc c c).
Induction c;Auto.
Save.
Hint refl_loose_eqc.
Lemma
refl_loose_eqc_cls: (c:cls)(Tfor_all2 ? ? loose_eqc c c).
(Induction c; Auto).
Save.
Hint refl_loose_eqc_cls.
Lemma
loose_eqc_trans: (c1,c2:class)(loose_eqc c1 c2)
->(c3:class)(loose_eqc c2 c3)->(loose_eqc c1 c3).
(Induction 1; Intros;Inversion_clear H0;Auto).
Save.
Inductive
adj_cls: class->class->Prop :=
adj_t: (s:skel)(adj_cls Trm (Typ s))
| adj_T: (s1,s2:skel)(adj_cls (Typ s1) (Knd s2)).
Hint adj_t adj_T.
Lemma
loose_eqc_stable: (t:term)(cl1,cl2:cls)
(Tfor_all2 ? ? loose_eqc cl1 cl2)
->(loose_eqc (cl_term t cl1) (cl_term t cl2)).
(Induction t; Simpl; Intros; Auto).
Generalize n .
(Elim H; Simpl; Intros; Auto).
(Case n0; Auto).
(Inversion_clear H0; Auto).
(Elim H0 with (TCs class (cl_term t0 cl1) cl1) (TCs class
(cl_term t0 cl2) cl2);
Auto).
(Elim H with cl1 cl2; Auto).
(Elim H with cl1 cl2; Auto; Intros).
(Elim s1; Elim s2; Elim H0 with cl1 cl2; Auto).
(Elim H0 with (TCs class (cl_term t0 cl1) cl1) (TCs class
(cl_term t0 cl2) cl2);
Auto).
(Elim H with cl1 cl2; Auto).
Save.
Hint loose_eqc_stable.
Lemma
cl_term_subst: (a:class)(G:cls)(x:term)(adj_cls (cl_term x G) a)
->(t:term)(k:nat)(E,F:cls)(TIns ? a k E F)
->(TTrunc ? k E G)
->(loose_eqc (cl_term t F) (cl_term (subst_rec x t k) E)).
(Induction t; Simpl; Intros; Auto).
(Elim (lt_eq_lt_dec k n); Simpl; Intros).
Elim y.
(Case n; Simpl; Intros).
Inversion_clear y0.
(Elim Tins_le with class k E F Trm a n0; Auto).
Induction 1.
(Rewrite -> (Tins_eq class k E F Trm a); Auto).
Apply loose_eqc_trans with (cl_term x G).
(Inversion_clear H; Auto).
(Elim cl_trunc with k E G x; Auto).
(Elim Tins_gt with class k E F Trm a n; Auto).
(Cut (loose_eqc (cl_term t0 F) (cl_term (subst_rec x t0 k) E));
Intros; Auto).
(Cut (loose_eqc (cl_term t1 (TCs class (cl_term t0 F) F))
(cl_term (subst_rec x t1 (S k))
(TCs class (cl_term (subst_rec x t0 k) E) E))); Intros).
(Elim H5; Auto; Intros).
(Elim H4; Auto).
(Apply loose_eqc_trans with (cl_term t1
(TCs ? (cl_term (subst_rec x t0 k) E) F));
Auto).
(Elim H0 with k E F; Auto; Intros).
(Elim s1; Elim s2; Elim H1 with k E F; Auto).
(Cut (loose_eqc (cl_term t0 F) (cl_term (subst_rec x t0 k) E));
Intros; Auto).
(Cut (loose_eqc (cl_term t1 (TCs class (cl_term t0 F) F))
(cl_term (subst_rec x t1 (S k))
(TCs class (cl_term (subst_rec x t0 k) E) E))); Intros).
(Elim H5; Auto; Intros).
(Elim H4; Auto).
(Apply loose_eqc_trans with (cl_term t1
(TCs ? (cl_term (subst_rec x t0 k) E) F));
Auto).
Save.
Lemma
class_knd: (e:env)(t,T:term)(typ e t T)->
T=(Srt kind)
->(cl_term t (class_env e))==(Knd (cv_skel (cl_term t (class_env e)))).
(Induction 1; Intros).
(Simpl; Auto).
(Elim H1; Intros).
(Elim item_trunc with term v e0 x; Auto; Intros).
(Elim wf_sort with v e0 x0 x; Auto; Intros).
Elim inv_typ_kind with e0 (Srt x1).
Elim H2.
Rewrite -> H3.
(Replace (Srt x1) with (lift (S v) (Srt x1)); Auto).
(Apply thinning_n with x0; Auto).
Discriminate H6.
(Elim type_case with e0 u (Prod V Ur); Auto; Intros).
Inversion_clear H5.
(Apply inv_typ_prod with e0 V Ur (Srt x); Auto).
Intros.
(Elim inv_typ_kind with e0 (Srt s2); Auto).
Elim H4.
(Replace (Srt s2) with (subst v (Srt s2)); Auto).
(Apply substitution with V; Auto).
Discriminate H5.
Simpl in H3.
Simpl.
(Rewrite -> H3; Auto).
(Elim (cl_term T0 (class_env e0)); Auto).
(Elim inv_typ_kind with e0 (Srt s); Auto).
(Elim H5; Auto).
Save.
Lemma
class_typ: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt kind))
->(cl_term t (class_env e))==(Typ (typ_skel (cl_term t (class_env e)))).
(Induction 1; Intros).
(Elim inv_typ_kind with e0 (Srt kind); Auto).
(Elim H1; Intros).
Simpl.
(Elim item_trunc with term v e0 x; Auto; Intros).
(Elim nth_class_env with x e0 x0 v; Auto).
(Elim cl_trunc with (S v) (class_env e0) (class_env x0) x; Auto).
Elim H3.
(Rewrite -> (class_knd e0 t0 (Srt kind)); Auto).
Simpl.
Simpl in H5.
Rewrite -> H5.
(Elim (cl_term T0 (class_env e0)); Intros; Auto).
(Apply inv_typ_prod with e0 T0 U (Srt kind); Intros; Auto).
(Elim conv_sort with s3 kind; Auto).
Simpl.
(Elim type_case with e0 u (Prod V Ur); Auto; Intros).
Inversion_clear H5.
Rewrite -> H3.
(Case (typ_skel (cl_term u (class_env e0))); Auto).
(Elim (cl_term v (class_env e0)); Auto).
(Apply inv_typ_prod with e0 V Ur (Srt x); Intros; Auto).
(Apply type_prod with s1; Auto).
(Elim conv_sort with s2 kind; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).
(Replace (Srt s2) with (subst v (Srt s2)); Auto).
(Apply substitution with V; Auto).
Discriminate H5.
Simpl.
Simpl in H3.
Rewrite -> H3;Auto.
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt kind) with (lift (S O) (Srt kind)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).
Apply H1.
(Elim type_case with e0 t0 U; Auto; Intros).
Inversion_clear H6.
(Elim conv_sort with x kind; Auto).
(Apply typ_conv_conv with e0 U V; Auto).
(Elim inv_typ_conv_kind with e0 V (Srt kind); Auto).
(Elim H6; Auto).
Save.
Lemma
class_typ_ord: (e:env)(T:term)(s:sort)(typ e T (Srt s))
->(P:class->Prop)(P (Typ (typ_skel (cl_term T (class_env e)))))
->(P (Knd (cv_skel (cl_term T (class_env e)))))
->(P (cl_term T (class_env e))).
(Destruct s; Intros).
(Rewrite -> (class_knd e T (Srt kind)); Auto).
(Rewrite -> (class_typ e T (Srt prop)); Auto).
Apply type_prop.
(Apply typ_wf with T (Srt prop); Auto).
Save.
Lemma
class_trm: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt prop))
->(cl_term t (class_env e))==Trm.
(Induction 1; Intros).
(Elim inv_typ_kind with e0 (Srt prop); Auto).
(Elim H1; Intros).
Simpl.
(Elim item_trunc with term v e0 x; Auto; Intros).
(Elim nth_class_env with x e0 x0 v; Auto).
(Elim cl_trunc with (S v) (class_env e0) (class_env x0) x; Auto).
Elim H3.
(Rewrite -> (class_typ e0 t0 (Srt prop)); Auto).
(Apply type_prop; Auto).
Simpl.
Simpl in H5.
(Rewrite -> H5; Auto).
(Apply inv_typ_prod with e0 T0 U (Srt prop); Intros; Auto).
(Elim conv_sort with s3 prop; Auto).
Simpl.
(Elim type_case with e0 u (Prod V Ur); Auto; Intros).
Inversion_clear H5.
(Rewrite -> H3; Auto).
(Apply inv_typ_prod with e0 V Ur (Srt x); Intros; Auto).
(Apply type_prod with s1; Auto).
(Elim conv_sort with s2 prop; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).
(Replace (Srt s2) with (subst v (Srt s2)); Auto).
(Apply substitution with V; Auto).
Discriminate H5.
Simpl.
Simpl in H3.
(Rewrite -> H3; Auto).
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt prop) with (lift (S O) (Srt prop)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).
Apply H1.
(Elim type_case with e0 t0 U; Auto; Intros).
Inversion_clear H6.
(Elim conv_sort with x prop; Auto).
(Apply typ_conv_conv with e0 U V; Auto).
(Elim inv_typ_conv_kind with e0 V (Srt prop); Auto).
(Elim H6; Auto).
Save.
Lemma
cl_term_sound: (e:env)(t,T:term)(typ e t T)->(K:term)(typ e T K)
->(adj_cls (cl_term t (class_env e)) (cl_term T (class_env e))).
Intros.
(Elim type_case with e t T; Intros; Auto).
Elim H1.
(Destruct x; Intros).
(Rewrite -> (class_knd e T (Srt kind)); Auto).
(Rewrite -> (class_typ e t T); Auto).
(Rewrite -> (class_typ e T (Srt prop)); Auto).
(Rewrite -> (class_trm e t T); Auto).
Apply type_prop.
(Apply typ_wf with t T; Auto).
(Elim inv_typ_kind with e K; Auto).
(Elim H1; Auto).
Save.
Lemma
cl_term_red1: (e:env)(A,T:term)(typ e A T)->(B:term)(red1 A B)
->(loose_eqc (cl_term A (class_env e)) (cl_term B (class_env e))).
(Induction 1; Intros; Auto).
Inversion_clear H1.
Inversion_clear H2.
Inversion_clear H6.
Simpl.
(Elim loose_eqc_stable with M (TCs class (cl_term T0 (class_env e0))
(class_env e0)) (TCs class
(cl_term M'
(class_env e0))
(class_env e0));
Auto).
(Elim H1 with M'; Auto).
Simpl.
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
(Elim H5 with M'; Auto).
(Elim (cl_term T0 (class_env e0)); Auto).
Generalize H2 H3 .
Clear H2 H3.
(Inversion_clear H4; Intros).
(Elim type_case with e0 (Abs T0 M) (Prod V Ur); Intros; Auto).
Inversion_clear H4.
(Apply inv_typ_prod with e0 V Ur (Srt x); Intros; Auto).
(Apply inv_typ_abs with e0 T0 M (Prod V Ur); Intros; Auto).
Simpl.
Apply loose_eqc_trans with (cl_term M (class_env (cons ? T0 e0))).
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
(Elim cl_term_sound with (cons ? T0 e0) M T1 (Srt s3); Intros; Auto).
(Elim (cl_term T0 (class_env e0)); Intros).
(Elim s4; Elim (cl_term v (class_env e0)); Auto).
(Elim s4; Elim (cl_term v (class_env e0)); Auto).
(Elim (cl_term v (class_env e0)); Auto).
Unfold subst.
(Apply cl_term_subst with (cl_term T0 (class_env e0)) (class_env e0);
Auto).
(Apply cl_term_sound with (Srt s0); Auto).
(Apply type_conv with V s0; Auto).
(Apply inv_conv_prod_l with Ur T1; Auto).
(Simpl; Auto).
Discriminate H4.
Simpl.
(Elim H4 with N1; Intros; Auto).
(Case s1; Case s2; Elim (cl_term v (class_env e0)); Auto).
Simpl.
(Elim (cl_term u (class_env e0)); Intros; Auto).
(Case s; Elim H1 with N2; Auto).
Inversion_clear H4.
Simpl.
(Elim loose_eqc_stable with U (TCs class (cl_term T0 (class_env e0))
(class_env e0)) (TCs class
(cl_term N1
(class_env e0))
(class_env e0));
Auto).
(Elim H1 with N1; Auto).
Simpl.
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
(Elim H3 with N2; Auto).
Save.
Lemma
cl_term_red: (T,U:term)(red T U)->(e:env)(K:term)(typ e T K)
->(loose_eqc (cl_term T (class_env e)) (cl_term U (class_env e))).
(Induction 1; Intros; Auto).
(Apply loose_eqc_trans with (cl_term P (class_env e)); Auto).
(Apply H1 with K; Auto).
(Apply cl_term_red1 with K; Auto).
(Apply subject_reduction with T; Auto).
Save.
Lemma
cl_term_conv: (e:env)(T,U,K1,K2:term)(typ e T K1)->(typ e U K2)
->(conv T U)
->(loose_eqc (cl_term T (class_env e)) (cl_term U (class_env e))).
Intros.
(Elim church_rosser with T U; Intros; Auto).
Apply loose_eqc_trans with (cl_term x (class_env e)).
(Apply cl_term_red with K1; Auto).
(Elim cl_term_red with U x e K2; Auto).
Save.
Lemma
skel_sound: (e:env)(t,T:term)(typ e t T)
->(cv_skel (cl_term T (class_env e)))==(typ_skel (cl_term t (class_env e))).
(Induction 1; Intros; Auto).
Inversion_clear H1.
Rewrite -> H2.
Simpl.
Clear H2 t0.
(Elim H3; Simpl; Intros).
Unfold lift.
(Elim cl_term_lift with (cl_term x (class_env l)) x O (class_env l) (
TCs class (cl_term x (class_env l)) (class_env l)); Auto).
(Elim (cl_term x (class_env l)); Auto).
Rewrite -> simpl_lift.
Unfold 1 lift.
(Elim cl_term_lift with (cl_term y (class_env l)) (lift (S n) x) O (
class_env l) (TCs class (cl_term y (class_env l)) (class_env l));
Auto).
Simpl.
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
Rewrite -> (commut_case ? ? cv_skel).
Rewrite -> (commut_case ? ? typ_skel).
Simpl.
(Replace (TCs class (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0)); Auto).
Pattern 1 (cl_term M (class_env (cons term T0 e0))) 1 (cl_term U
(class_env
(cons term T0
e0))) .
(Elim cl_term_sound with (cons ? T0 e0) M U (Srt s2); Intros; Auto).
Rewrite -> (commut_case ? ? cv_skel).
Rewrite -> (commut_case ? ? typ_skel).
(Elim (cl_term T0 (class_env e0)); Auto).
(Elim H5; Auto).
(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
Inversion_clear H4.
(Apply inv_typ_prod with e0 V Ur (Srt x); Intros; Auto).
Unfold subst.
Generalize H3 .
Cut (adj_cls (cl_term u (class_env e0))
(cl_term (Prod V Ur) (class_env e0))).
Simpl.
(Elim cl_term_subst with (cl_term V (class_env e0)) (class_env e0) v Ur O (
class_env e0) (TCs class (cl_term V (class_env e0)) (class_env e0));
Simpl; Auto).
Intros.
Inversion_clear H8.
Intros.
Inversion_clear H8.
Auto.
(Elim cl_term_sound with e0 v V (Srt s1); Simpl; Intros; Auto).
Rewrite -> H9.
(Inversion_clear H8; Auto).
(Elim s3; Auto).
Generalize H9 .
(Inversion_clear H8; Intros; Auto).
Simpl in H8.
(Elim H8; Auto).
(Apply cl_term_sound with (Srt s1); Auto).
(Apply cl_term_sound with (Srt x); Auto).
Discriminate H4.
Simpl.
Simpl in H3.
Simpl in H1.
Rewrite -> (commut_case ? ? typ_skel).
Simpl.
Elim H3.
(Elim (cl_term U (TCs class (cl_term T0 (class_env e0)) (class_env e0)));
Auto).
(Elim (cl_term T0 (class_env e0)); Auto).
Elim H1.
(Elim cl_term_conv with e0 U V (Srt s) (Srt s); Auto).
(Elim type_case with e0 t0 U; Auto; Intros).
Inversion_clear H5.
(Elim conv_sort with x s; Auto).
(Apply typ_conv_conv with e0 U V; Auto).
(Elim inv_typ_conv_kind with e0 V (Srt s); Auto).
(Elim H5; Auto).
Save.
(* Strict stability results *)
Inductive
typ_cls: class->class->Prop :=
tc_t: (typ_cls Trm (Typ PROP))
| tc_T: (s:skel)(typ_cls (Typ s) (Knd s)).
Hint tc_t tc_T.
Lemma
class_subst: (a:class)(G:cls)(x:term)(typ_cls (cl_term x G) a)
->(t:term)(k:nat)(E,F:cls)(TIns ? a k E F)
->(TTrunc ? k E G)
->(cl_term t F)==(cl_term (subst_rec x t k) E).
(Induction t; Simpl; Intros; Auto).
(Elim (lt_eq_lt_dec k n); Simpl; Intros).
Elim y.
(Case n; Simpl; Intros).
Inversion_clear y0.
(Elim Tins_le with class k E F Trm a n0; Auto).
Induction 1.
(Rewrite -> (Tins_eq class k E F Trm a); Auto).
Replace (cl_term (lift k x) E) with (cl_term x G).
(Inversion_clear H; Auto).
Symmetry.
(Apply cl_trunc; Auto).
(Elim Tins_gt with class k E F Trm a n; Auto).
(Elim H0 with k E F; Auto).
(Elim H1 with (S k) (TCs class (cl_term t0 F) E) (TCs class
(cl_term t0 F) F);
Auto).
(Elim H0 with k E F; Auto).
(Elim H1 with k E F; Auto).
(Elim H0 with k E F; Auto).
(Elim H1 with (S k) (TCs class (cl_term t0 F) E) (TCs class
(cl_term t0 F) F);
Auto).
Save.
Lemma
class_sound: (e:env)(t,T:term)(typ e t T)->(K:term)(typ e T K)
->(typ_cls (cl_term t (class_env e)) (cl_term T (class_env e))).
Intros.
(Elim type_case with e t T; Intros; Auto).
Elim H1.
(Destruct x; Intros).
(Rewrite -> (class_knd e T (Srt kind)); Auto).
(Rewrite -> (class_typ e t T); Auto).
(Elim skel_sound with e t T; Auto).
(Rewrite -> (class_typ e T (Srt prop)); Auto).
(Rewrite -> (class_trm e t T); Auto).
(Elim skel_sound with e T (Srt prop); Simpl; Auto).
Apply type_prop.
(Apply typ_wf with t T; Auto).
Elim inv_typ_kind with e K.
(Elim H1; Auto).
Save.
Lemma
class_red: (e:env)(T,U,K:term)(typ e T K)->(red T U)
->(cl_term T (class_env e))==(cl_term U (class_env e)).
Intros.
Cut (eqT ? (typ_skel (cl_term T (class_env e)))
(typ_skel (cl_term U (class_env e)))).
(Elim cl_term_red with T U e K; Simpl; Intros; Auto).
(Elim H1; Auto).
(Elim skel_sound with e T K; Auto).
(Apply skel_sound; Auto).
(Apply subject_reduction with T; Auto).
Save.
13/02/97, 13:19