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