Interp.v

Require Termes.
Require Conv.
Require Types.
Require Class.
Require Skel.
Require Can.


  Definition intt := nat->term.

  Definition shift_intt : intt->term->intt :=
     [i:intt][t:term][n:nat]Cases n of
         O => t
       | (S k) => (i k)
       end.

  Fixpoint int_term [t:term]: intt->nat->term :=
    [I:intt][k:nat]Cases t of
       (Srt s) => (Srt s)
     | (Ref n) => Case (le_gt_dec k n) of
                    [_:(le k n)](lift k (I (minus n k)))
                    [_:(gt k n)](Ref n)
                  end
     | (Abs A t) => (Abs (int_term A I k) (int_term t I (S k)))
     | (App u v) => (App (int_term u I k) (int_term v I k))
     | (Prod A B) => (Prod (int_term A I k) (int_term B I (S k)))
     end.

  Lemma int_term_subst: (t:term)(it:intt)(k:nat)(x:term)
       (subst_rec x (int_term t it (S k)) k)=(int_term t (shift_intt it x) k).
Induction t;Simpl;Intros;Auto.
Elim (le_gt_dec (S k) n);Intros.
Elim (le_gt_dec k n);Intros.
(Rewrite -> simpl_subst;Auto).
(Replace (minus n k) with (S (minus n (S k)));Auto).
(Rewrite -> minus_Sn_m;Auto).

Elim le_not_gt with k n ;Auto.

Simpl.
Elim (lt_eq_lt_dec k n);Intros.
Elim y0;Intros.
Absurd (le n k);Auto.

Elim (le_gt_dec k n);Intros;Auto.
Elim y1.
Replace (minus k k) with O;Auto.

Inversion_clear y1 in y2.
Elim gt_antirefl with n ;Auto.

Elim (le_gt_dec k n);Intros;Auto.
Absurd (le k n);Auto.

Rewrite -> H;Rewrite -> H0;Auto.

Rewrite -> H;Rewrite -> H0;Auto.

Rewrite -> H;Rewrite -> H0;Auto.
Save.

  Fixpoint int_typ [T:term]: env->intP->(s:skel)(Can s) :=
   [e:env][ip:intP][s:skel]Cases T of
      (Srt _) => (default_can s)
    | (Ref n) => (extract_CR s (Tnth_def Int_K (iK PROP sn) ip n))
    | (Abs A t) => Cases (cl_judge e A) of
                     Ord => <[s0:skel](Can s0)>Case s of
                              (default_can PROP)
                              [s1,s2:skel][C:(Can s1)](int_typ t (cons ? A e)
                                                    (TCs ? (iK s1 C) ip) s2)
                              end
                   | Typ => (int_typ t (cons ? A e)
                                          (def_cons (class_env e) A ip) s)
                   | _ =>(default_can s)
                   end
    | (App u v) => Cases (cl_judge e u) (cl_judge e v) of
                     Typ Trm => (int_typ u e ip s)
                   | Typ Typ => ((int_typ u e ip (PROD (typ_skel v e) s))
                                             (int_typ v e ip (typ_skel v e)))
                   | _ _ => (default_can s)
                   end
    | (Prod A B) => <[s0:skel](Can s0)>Case s of
                        ([s:skel](Pi s ([C:(Can s)](int_typ B (cons ? A e)
                             (TCs ? (iK s C) ip) PROP)) (int_typ A e ip PROP))
                         (cv_skel A (class_env e)))
                        [s1,s2:skel](default_can (PROD s1 s2))
                        end
    end.

  Lemma int_equiv_int_typ: (T:term)(i,i':intP)(int_eq_can i i')
           ->(s:skel)(e:env)(eq_can s (int_typ T e i s) (int_typ T e i' s)).
(Induction T; Simpl; Intros; Auto).
Generalize n .
(Elim H; Auto).
Unfold Tnth_def .
Intros.
Apply eq_can_extr.
(Simpl; Auto).

(Destruct n; Intros).
Unfold Tnth_def .
Apply eq_can_extr.
Auto.

(Simpl; Auto).

(Elim (cl_judge e t); Simpl; Auto).
(Unfold def_cons ; Auto).

(Case s; Simpl; Auto).

(Elim (cl_judge e t); Simpl; Auto).
(Elim (cl_judge e t0); Simpl; Auto).
Generalize (H i i' H1 (PROD (typ_skel t0 e) s) e) .
(Simpl; Intros).
(Apply H2; Auto).
(Apply H0; Auto).
(Elim H1; Auto).

(Apply H0; Auto).
(Elim H1; Auto).

(Case s; Simpl; Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
Save.

  Hint int_equiv_int_typ.

  Lemma int_typ_red1_env: (e:env)(t,T:term)(typ e t T)
                  ->(s:skel)(ip:intP)(int_inv ip)
                   ->(f:env)(red1_in_env e f)
                    ->(eq_can s (int_typ t e ip ?) (int_typ t f ip ?)).
(Induction 1; Intros).
(Simpl; Auto).

Simpl.
Generalize v .
Elim H2.
Unfold Tnth_def .
Intro.
Intros.
(Apply eq_can_extr; Simpl; Auto).

Destruct v.
Unfold Tnth_def .
(Apply eq_can_extr; Auto).

(Simpl; Auto).

Simpl.
Unfold cl_judge .
(Elim class_env_red1 with e0 f; Auto).
Unfold def_cons .
(Elim (cl_term T0 (class_env e0)); Auto).
(Case s; Simpl; Auto; Intros).
(Apply eq_can_trans with (int_typ M (cons term T0 f)
                           (TCs Int_K (iK s0 X1) ip) s3);
Auto).

(Apply typ_wf with T0 (Srt s1); Auto).

Simpl.
(Cut (wf e0); Intros).
Unfold cl_judge .
(Elim class_env_red1 with e0 f; Auto).
(Elim (cl_term u (class_env e0)); Simpl; Auto).
(Elim (cl_term v (class_env e0)); Auto).
Generalize (H3 (PROD (typ_skel v e0) s) ip H4 f H5) .
(Simpl; Intros).
(Elim typ_skel_red_env with e0 v V f; Auto).

(Apply typ_wf with v V; Auto).

Simpl.
(Cut (wf e0); Intros).
(Elim s; Auto; Intros).
(Elim class_env_red1 with e0 f; Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U (cons term T0 f)
                           (TCs Int_K
                             (iK (cv_skel T0 (class_env e0)) X1) ip)
                           PROP);
Auto).

(Simpl; Auto).

(Apply typ_wf with T0 (Srt s1); Auto).

Auto.
Save.

  Lemma nth_lift_int: (y:Int_K)(s0:skel)(ipe,ipf:intP)(n,k:nat)(e,f:env)
       (TIns ? y k ipe ipf)
         -> (int_typ (lift_rec (S O) (Ref n) k) f ipf s0)
              ==(int_typ (Ref n) e ipe s0).
(Simpl; Intros).
Elim (le_gt_dec k n).
Generalize n .
(Elim H; Simpl; Auto).
(Destruct n0; Intros; Auto).
Inversion_clear y1.

Generalize n .
(Elim H; Simpl; Auto).
Intros.
Inversion_clear y0.

(Destruct n0; Intros; Auto).
Save.

  Lemma lift_int_typ: (y:Int_K)(x,T:term)(k:nat)(e,f:env)
        (ins_in_env x k e f)
         ->(ipe,ipf:intP)(TIns ? y k ipe ipf)
          ->(int_inv ipf)
           ->(s:skel)(eq_can s (int_typ T e ipe s)
                               (int_typ (lift_rec (S O) T k) f ipf s)).
Induction y.
Induction T.
(Simpl; Auto).

Intros.
(Elim nth_lift_int with (iK s c) s0 ipe ipf n k e f; Intros; Auto).

(Simpl; Intros).
(Elim cl_judge_lift with e f k x t; Auto).
(Elim (cl_judge e t); Auto).
Unfold def_cons .
(Elim cv_skel_lift with (cl_judge e (lift k x)) t (class_env e) (
class_env f) k; Auto).
(Apply class_env_lift; Auto).

(Case s0; Simpl; Intros; Auto).
(Apply eq_can_trans with (int_typ (lift_rec (S O) t0 (S k))
                           (cons ? (lift_rec (S O) t k) f)
                           (TCs ? (iK s1 X1) ipf) s2);
Auto).

(Simpl; Intros).
(Elim cl_judge_lift with e f k x t; Auto).
(Elim (cl_judge e t); Auto).
(Elim cl_judge_lift with e f k x t0; Auto).
(Elim typ_skel_lift with t0 k e f x; Auto).
(Elim (cl_judge e t0); Auto).
Generalize (H k e f H1 ipe ipf H2 H3 (PROD (typ_skel t0 e) s0)) .
(Simpl; Intros; Auto).
(Apply H4; Auto).
Apply int_equiv_int_typ.
Apply int_inv_int_eq_can.
(Apply ins_int_inv with ipf k (iK s c); Auto).

(Simpl; Intros).
(Case s0; Simpl; Intros; Auto).
(Elim cv_skel_lift with (cl_judge e (lift k x)) t (class_env e) (
class_env f) k; Auto).
(Apply eq_Pi; Auto).
(Simpl; Intros).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ (lift_rec (S O) t0 (S k))
                           (cons term (lift_rec (S O) t k) f)
                           (TCs Int_K (iK (cv_skel t (class_env e)) X1)
                             ipf)
                           PROP);
Auto).

(Apply class_env_lift; Auto).
Save.

  Lemma subst_int_typ: (g:env)(v,V:term)(typ g v V)->(cl_judge g v)=Typ
        ->(ipg:intP)(e:env)(T,K:term)(typ e T K)
         ->(k:nat)(f:env)(ipe,ipf:intP)(trunc ? k f g)->(sub_in_env v V k e f)
          ->(TTrunc ? k ipf ipg)
           ->(TIns ? (iK (typ_skel v g) (int_typ v g ipg (typ_skel v g))) k
                         ipf ipe)
            ->(int_inv ipe)
             ->(eq_can (typ_skel T e) (int_typ T e ipe (typ_skel T e))
                         (int_typ (subst_rec v T k) f ipf (typ_skel T e))).
Do 6 Intro.
Cut (lift_cls (cl_judge g v) (cl_judge g V)).
(Induction 2; Intros; Auto).
(Simpl; Auto).

Elim (lt_eq_lt_dec k v0).
Destruct y.
(Case v0; Intros).
Inversion_clear l.

(Rewrite -> subst_ref_gt; Auto).
Unfold pred .
(Elim nth_lift_int with (iK (typ_skel v g)
                          (int_typ v g ipg (typ_skel v g))) (typ_skel
                                                              (
                                                             Ref (S n))
                                                              e0) ipf ipe n k f e0;
Auto).
(Rewrite -> lift_ref_ge; Auto).

Induction 1.
Rewrite -> subst_ref_eq.
Generalize e0 f H5 H6 H7 H9 .
Clear H9 H7 H6 H5 H4 H3 H2 y f t K T e.
(Elim H8; Intros).
Generalize H5 .
(Inversion_clear H6; Intros).
Inversion_clear H2.
Rewrite -> lift0.
Unfold 1 4 5 typ_skel .
Unfold 1 int_typ .
Unfold Tnth_def .
Generalize H7 .
Inversion H9.
Intro.
Rewrite -> (skel_sound g v V).
Pattern (typ_skel v g) (extract_CR (typ_skel v g)
                         (iK (typ_skel v g)
                           (int_typ v g ipg (typ_skel v g)))) .
(Apply extr_eq with (int_typ v g ipg (typ_skel v g)); Auto).
Inversion_clear H11.
Change <Prop>
         Case
         (existT skel [s:skel](Can s) (typ_skel v g)
           (int_typ v g ipg (typ_skel v g)))
         of [s:skel][C:(Can s)](eq_can s C C)
            end.
(Elim H3; Auto).

Auto.

Generalize H5 .
(Inversion_clear H6; Intros).
Inversion_clear H6.
Inversion_clear H7.
Rewrite -> simpl_lift.
Change (eq_can (typ_skel (Ref n) e)
         (int_typ (Ref n) e il (typ_skel (Ref n) e))
         (int_typ (lift (S O) (lift n v))
           (cons term (subst_rec v u n) f0) (TCs Int_K y l)
           (typ_skel (Ref n) e))).
Apply eq_can_trans with (int_typ (lift n v) f0 l (typ_skel (Ref n) e)).
(Inversion H9; Auto).

(Inversion H9; Auto).
Apply int_equiv_int_typ.
Apply int_inv_int_eq_can.
(Apply ins_int_inv with il n (iK (typ_skel v g)
                               (int_typ v g ipg (typ_skel v g)));
Auto).

Unfold 2 lift .
(Apply lift_int_typ with y (subst_rec v u n); Auto).
(Inversion H9; Auto).
(Cut (int_inv l); Auto).
(Apply ins_int_inv with il n (iK (typ_skel v g)
                               (int_typ v g ipg (typ_skel v g)));
Auto).

Intros.
(Rewrite -> subst_ref_lt; Auto).
(Elim nth_lift_int with (iK (typ_skel v g)
                          (int_typ v g ipg (typ_skel v g))) (typ_skel
                                                              (
                                                             Ref v0) e0) ipf ipe v0 k f e0;
Auto).
(Rewrite -> lift_ref_lt; Auto).

Clear H4 H6.
Cut (eq ? (cl_judge (cons ? T0 e0) U) Typ)
     ->(eqT ? (typ_skel M (cons ? T0 e0)) PROP).
Simpl.
(Elim corr_lift with (cons ? T0 e0) M U (Srt s2); Auto).
(Elim cl_judge_subst with g v V k e0 f T0; Auto).
(Elim (cl_judge e0 T0); Auto).
Unfold def_cons .
(Elim cv_skel_subst with g v V T0 k e0 f; Auto).
(Induction 1; Auto).

(Simpl; Auto).

(Elim cl_judge_subst with g v V k e0 f T0; Auto).
(Elim (cl_judge e0 T0); Auto).
Unfold def_cons .
(Elim cv_skel_subst with g v V T0 k e0 f; Auto).

(Simpl; Intros).
(Apply eq_can_trans with (int_typ M (cons term T0 e0)
                           (TCs Int_K
                             (iK (cv_skel T0 (class_env e0)) X2) ipe)
                           (typ_skel M (cons term T0 e0)));
Auto).

Intro.
(Elim skel_sound with (cons ? T0 e0) M U; Auto).
(Apply skel_not_ord with (Srt s2); Auto).
Rewrite -> H4.
(Unfold cl_judge ; Auto).

(Elim type_case with e0 u (Prod V0 Ur); Intros; Auto).
(Elim H12; Intros).
Clear H12.
(Apply inv_typ_prod with e0 V0 Ur (Srt x); Auto; Intros).
Cut (eq ? (cl_judge e0 (Prod V0 Ur)) Ord)
     ->(eq ? (cl_judge e0 V0) Ord)
        ->(eqT ? (typ_skel u e0)
            (PROD (typ_skel v0 e0) (predr (typ_skel u e0)))).
Simpl.
(Elim cl_judge_subst with g v V k e0 f u; Auto).
(Elim cl_judge_subst with g v V k e0 f v0; Auto).
(Elim typ_skel_subst with g v V v0 k e0 f; Auto).
(Elim corr_lift with e0 u (Prod V0 Ur) (Srt x); Auto).
(Elim corr_lift with e0 v0 V0 (Srt s1); Auto).
Intro.
Generalize (H6 k f ipe ipf H7 H8 H9 H10 H11) .
(Rewrite -> H16; Auto).
(Simpl; Intros).
(Apply H17; Auto).
(Cut (int_inv ipf); Auto).
(Apply ins_int_inv with ipe k (iK (typ_skel v g)
                                (int_typ v g ipg (typ_skel v g)));
Auto).

(Symmetry; Apply skel_sound; Auto).

(Elim skel_sound with e0 u (Prod V0 Ur); Auto).
(Elim skel_sound with e0 v0 V0; Auto).
Simpl.
(Unfold cl_judge ; Simpl).
Intros.
Rewrite -> H16.
(Rewrite -> H17; Auto).

Discriminate H12.

Simpl.
(Elim cv_skel_subst with g v V T0 k e0 f; Auto).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U (cons term T0 e0)
                           (TCs Int_K
                             (iK (cv_skel T0 (class_env e0)) X2) ipe)
                           PROP);
Auto).
(Replace PROP with (typ_skel U (cons ? T0 e0)); Auto).
(Elim skel_sound with (cons ? T0 e0) U (Srt s2); Auto).

(Replace PROP with (typ_skel T0 e0); Auto).
(Elim skel_sound with e0 T0 (Srt s1); Auto).

(Elim type_case with g v V; Intros; Auto).
(Elim H1; Intros).
(Apply corr_lift with (Srt x); Auto).

(Rewrite -> H1; Rewrite -> H0; Auto).
Save.

  Lemma subst_int_typ_trm: (g:env)(v,V:term)(typ g v V)->(cl_judge g v)=Trm
              ->(y:Int_K)(e:env)(T,K:term)(typ e T K)
               ->(k:nat)(f:env)(ipe,ipf:intP)(trunc ? k f g)
                ->(sub_in_env v V k e f)->(TIns ? y k ipf ipe)->(int_inv ipe)
                 ->~(cl_judge e T)=Trm
                  ->(eq_can (typ_skel T e) (int_typ T e ipe ?)
                            (int_typ (subst_rec v T k) f ipf ?)).

Do 6 Intro.
Cut (lift_cls (cl_judge g v) (cl_judge g V)).
(Induction 2; Auto; Intros).
(Simpl; Auto).

Elim (lt_eq_lt_dec k v0).
Destruct y.
(Case v0; Intros).
Inversion_clear l.

(Rewrite -> subst_ref_gt; Auto).
Unfold pred .
(Elim nth_lift_int with y (typ_skel (Ref (S n)) e0) ipf ipe n k f e0;
Auto).
(Rewrite -> lift_ref_ge; Auto).

Intro.
Elim H9.
Elim e1.
Unfold cl_judge .
Simpl.
Replace (nth_def class Trm (class_env e0) k) with (cl_judge g V).
Generalize H0 .
(Elim H1; Intros; Auto).

Generalize H5 .
(Elim H6; Simpl; Auto).
Intros.
(Inversion_clear H10; Auto).

(Simpl; Intros).
(Inversion_clear H12; Auto).

Intros.
(Rewrite -> subst_ref_lt; Auto).
(Elim nth_lift_int with y (typ_skel (Ref v0) e0) ipf ipe v0 k f e0; Auto).
(Rewrite -> lift_ref_lt; Auto).

Clear H4 H6.
Generalize H13 .
(Replace (cl_judge e0 (Abs T0 M)) with (cl_judge (cons ? T0 e0) M); Auto).
Simpl.
(Elim corr_lift with (cons ? T0 e0) M U (Srt s2); Auto).
(Induction 1; Auto).

(Elim cl_judge_subst with g v V k e0 f T0; Auto).
(Elim (cl_judge e0 T0); Auto).
Intro.
Unfold def_cons .
(Elim cv_skel_subst with g v V T0 k e0 f; Auto).

(Simpl; Intros).
(Apply eq_can_trans with (int_typ M (cons term T0 e0)
                           (TCs Int_K
                             (iK (cv_skel T0 (class_env e0)) X2) ipe)
                           (typ_skel M (cons term T0 e0)));
Auto).

(Elim type_case with e0 u (Prod V0 Ur); Intros; Auto).
(Elim H12; Intros).
Clear H12.
(Apply inv_typ_prod with e0 V0 Ur (Srt x); Auto; Intros).
Cut (eq ? (cl_judge e0 (Prod V0 Ur)) Ord)
     ->(eq ? (cl_judge e0 V0) Ord)
        ->(eqT ? (typ_skel u e0)
            (PROD (typ_skel v0 e0) (predr (typ_skel u e0)))).
Generalize H4 .
Simpl.
(Elim cl_judge_subst with g v V k e0 f u; Auto).
(Elim cl_judge_subst with g v V k e0 f v0; Auto).
(Elim typ_skel_subst with g v V v0 k e0 f; Auto).
(Elim corr_lift with e0 u (Prod V0 Ur) (Srt x); Auto).
(Elim corr_lift with e0 v0 V0 (Srt s1); Auto).
Intros.
Generalize (H6 k f ipe ipf H7 H8 H9 H10 H11) .
Clear H4 H6.
(Rewrite -> H17; Auto).
(Simpl; Intros).
(Cut (int_inv ipf); Auto; Intros).
(Apply H4; Auto).
(Apply H16; Auto).
Discriminate.

(Apply ins_int_inv with ipe k y; Auto).

(Symmetry; Apply skel_sound; Auto).

(Elim skel_sound with e0 u (Prod V0 Ur); Auto).
(Elim skel_sound with e0 v0 V0; Auto).
(Unfold cl_judge ; Simpl).
Intros.
Rewrite -> H16.
(Rewrite -> H17; Auto).

Discriminate H12.

Simpl.
(Elim cv_skel_subst with g v V T0 k e0 f; Auto).
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U (cons term T0 e0)
                           (TCs Int_K
                             (iK (cv_skel T0 (class_env e0)) X2) ipe)
                           PROP);
Auto).
(Replace PROP with (typ_skel U (cons ? T0 e0)); Auto).
(Elim skel_sound with (cons ? T0 e0) U (Srt s2); Auto).

(Replace PROP with (typ_skel T0 e0); Auto).
(Apply H4; Auto).
Generalize H3 .
(Case s1; Intros).
(Rewrite -> class_ord; Auto).
Discriminate.

(Rewrite -> (class_typ e0 T0 (Srt prop)); Auto).
Discriminate.

Apply type_prop.
(Apply typ_wf with T0 (Srt prop); Auto).

(Elim skel_sound with e0 T0 (Srt s1); Auto).

(Elim type_case with g v V; Intros; Auto).
(Elim H1; Intros).
(Apply corr_lift with (Srt x); Auto).

Generalize H0 .
(Rewrite -> (class_ord g v); Intros).
Discriminate H2.

(Elim H1; Auto).
Save.

  Lemma int_typ_red1: (e:env)(U,K:term)(typ e U K)
         ->(V:term)(red1 U V)->(ip:intP)(int_inv ip)
          ->~(cl_judge e U)=Trm
           ->(eq_can (typ_skel U e) (int_typ U e ip ?) (int_typ V e ip ?)).
(Induction 1; Auto; Intros).
Inversion_clear H1.

Inversion_clear H2.

Inversion_clear H6.
Simpl.
(Elim cl_judge_red with e0 T (Srt s1) M'; Auto).
(Elim (cl_judge e0 T); Simpl; Auto).
Unfold def_cons .
(Elim skel_red1 with e0 T (Srt s1) M'; Auto).
(Apply int_typ_red1_env with U0; Auto).

(Elim (cl_judge (cons term T e0) M); Simpl; Auto).
Intros.
(Apply eq_can_trans with (int_typ M (cons term M' e0)
                           (TCs Int_K
                             (iK (cv_skel T (class_env e0)) X1) ip)
                           (typ_skel M (cons ? T e0)));
Auto).
(Apply int_typ_red1_env with U0; Auto).

Simpl.
(Elim (cl_judge e0 T); Simpl; Auto).
Generalize H5 .
Clear H1 H3 H5.
(Cut (not (eq ? (cl_judge (cons ? T e0) M) Trm)); Auto).
(Elim corr_lift with (cons ? T e0) M U0 (Srt s2); Auto).
(Induction 1; Auto).

Intros.
Unfold def_cons .
(Apply H5; Auto).

(Elim (cl_judge (cons term T e0) M); Simpl; Auto).
Intros.
(Apply eq_can_trans with (int_typ M (cons term T e0)
                           (TCs Int_K
                             (iK (cv_skel T (class_env e0)) X2) ip)
                           (typ_skel M (cons term T e0)));
Auto).

(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
Inversion_clear H7.
(Apply inv_typ_prod with e0 V Ur (Srt x); Auto; Intros).
Cut (eq ? (cl_judge e0 (Prod V Ur)) Ord)
     ->(eq ? (cl_judge e0 V) Ord)
        ->(eqT ? (typ_skel u e0)
            (PROD (typ_skel v e0) (predr (typ_skel u e0)))).
Generalize H2 H3 H6 .
Clear H2 H3 H6.
(Replace (cl_judge e0 (App u v)) with (cl_judge e0 u); Auto).
(Inversion_clear H4; Intros).
(Apply inv_typ_abs with e0 T M (Prod V Ur); Auto; Intros).
(Cut (typ e0 v T); Intros).
Generalize H6 (subst_int_typ e0 v T H15) (subst_int_typ_trm e0 v T H15) .
Clear H1 H3.
Simpl.
(Replace (cl_judge e0 (Abs T M)) with (cl_judge (cons ? T e0) M); Auto).
(Elim corr_lift with (cons ? T e0) M T0 (Srt s3); Auto).
(Induction 1; Auto).

(Elim corr_lift with e0 v T (Srt s0); Auto).
Intros.
Clear H4 H1 H3.
Unfold def_cons subst .
(Apply H16 with (iK (cv_skel T (class_env e0))
                  (default_can (cv_skel T (class_env e0)))) T0;
Auto).

Intros.
Simpl.
Clear H4 H1 H16.
Unfold subst .
(Apply H3 with ip T0; Auto).

(Apply type_conv with V s0; Auto).
(Apply inv_conv_prod_l with Ur T0; Auto).

Generalize H4 H11 .
Clear H1 H4 H6 H11.
Simpl.
(Elim cl_judge_red with e0 u (Prod V Ur) N1; Auto).
(Elim cl_judge_red with e0 u (Prod V Ur) N1; Auto).
(Elim corr_lift with e0 v V (Srt s1); Auto).
(Elim corr_lift with e0 u (Prod V Ur) (Srt x); Auto).
Intros.
(Apply H4; Auto).
Discriminate.

(Elim corr_lift with e0 u (Prod V Ur) (Srt x); Auto).
Intros.
Generalize (H4 N1 H2 ip H5) .
(Rewrite -> H11; Auto).
(Simpl; Intros).
(Apply H1; Auto).
Discriminate.

Generalize H1 .
Clear H1 H4 H6 H11.
Simpl.
(Elim typ_skel_red1 with e0 v N2 V; Auto).
(Elim cl_judge_red with e0 v V N2; Auto).
(Elim corr_lift with e0 v V (Srt s1); Auto).
(Elim corr_lift with e0 u (Prod V Ur) (Srt x); Auto).

(Elim corr_lift with e0 u (Prod V Ur) (Srt x); Auto).
Intros.
(Cut (eq_can (PROD (typ_skel v e0) (predr (typ_skel u e0)))
       (int_typ u e0 ip (PROD (typ_skel v e0) (predr (typ_skel u e0))))
       (int_typ u e0 ip (PROD (typ_skel v e0) (predr (typ_skel u e0)))));
Auto).
(Simpl; Intros).
(Apply H4; Auto).
(Apply H1; Auto).
Discriminate.

(Elim skel_sound with e0 u (Prod V Ur); Auto).
(Elim skel_sound with e0 v V; Auto).
(Unfold cl_judge ; Simpl).
Intros.
Rewrite -> H11.
(Rewrite -> H12; Auto).

Discriminate H7.

(Cut (not (eq ? (cl_judge e0 T) Trm)); Intros).
(Cut (eqT ? (typ_skel T e0) PROP); Intros).
(Cut (eqT ? (typ_skel U0 (cons ? T e0)) PROP); Intros).
Unfold typ_skel .
Inversion_clear H4.
Simpl.
(Replace eq_cand with (eq_can PROP); Auto).
(Elim skel_red1 with e0 T (Srt s1) N1; Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U0 (cons ? T e0)
                           (TCs Int_K
                             (iK (cv_skel T (class_env e0)) X2) ip)
                           PROP);
Auto).
Elim H9.
(Apply int_typ_red1_env with (Srt s2); Auto).

(Elim H8; Auto).

Simpl.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_Pi; Auto).
Simpl.
Intros.
(Replace eq_cand with (eq_can PROP); Auto).
(Apply eq_can_trans with (int_typ U0 (cons ? T e0)
                           (TCs Int_K
                             (iK (cv_skel T (class_env e0)) X2) ip)
                           PROP);
Auto).
(Elim H9; Auto).

(Elim skel_sound with (cons ? T e0) U0 (Srt s2); Auto).

(Elim skel_sound with e0 T (Srt s1); Auto).

Generalize H0 .
(Elim s1; Intros).
(Rewrite -> (class_ord e0 T); Auto).
Discriminate.

(Rewrite -> (class_typ e0 T (Srt prop)); Auto).
Discriminate.

Apply type_prop.
(Apply typ_wf with T (Srt prop); Auto).
Save.

  Lemma red_int_typ: (e:env)(U,K:term)(typ e U K)->~(cl_judge e U)=Trm
            ->(ip:intP)(int_inv ip)->(V:term)(red U V)
              ->(eq_can (typ_skel U e) (int_typ U e ip ?) (int_typ V e ip ?)).
Induction 4;Auto;Intros.
Apply eq_can_trans with (int_typ P e ip (typ_skel U e)) ;Auto.
Replace (typ_skel U e) with (typ_skel P e).
(Apply int_typ_red1 with K ;Auto).
Apply subject_reduction with U ;Auto.

(Elim cl_judge_red with e U K P ;Auto).

Elim skel_sound with e U K ;Auto.
Elim skel_sound with e P K ;Auto.
Apply subject_reduction with U ;Auto.
Save.

  Lemma conv_int_typ: (e:env)(U,V,K:term)(conv U V)
           ->(typ e U K)->(typ e V K)
            ->~(cl_judge e U)=Trm->(ip:intP)(int_inv ip)
             ->(eq_can (typ_skel U e) (int_typ U e ip ?) (int_typ V e ip ?)).
Intros.
Elim church_rosser with U V ;Intros;Auto.
Apply eq_can_trans with (int_typ x e ip (typ_skel U e)) ;Auto.
Apply red_int_typ with K ;Auto.

Apply eq_can_sym.
Replace (typ_skel U e) with (typ_skel V e).
Apply red_int_typ with K ;Auto.
Rewrite -> (cl_judge_red e V K H1 x);Auto.
Elim cl_judge_red with e U K x ;Auto.

(Elim skel_sound with e U K ;Auto).
(Elim skel_sound with e V K ;Auto).
Save.

20/01/97, 14:44