Library Class





Require
 Export
 Can.

Require
 Export
 Types
.

Require
 Export
 IntMap.




  Inductive
 class : Set
 :=

    | Trm : class

    | Typ : skel -> class

    | Knd : skel -> class.




  Definition
 cls := nat -> class.

  Definition
 nil_cls : cls := fun
 _
 => Typ PROP.




  Definition
 Knd_1 c
 := match
 c
 with


                        | Knd s
 => s


                        | _
 => PROP

                        end
.




  Definition
 Typ_1 c
 := match
 c
 with


                        | Typ s
 => s


                        | _
 => PROP

                        end
.




  Lemma
 commut_case :

   forall
 (A
 B
 : Type
) (f
 : A
 -> B
) c
 bt
 bT
 bK
,

   f
 match
 c
 with


     | Trm => bt


     | Typ s
 => bT
 s


     | Knd s
 => bK
 s


     end
 =

   match
 c
 with


   | Trm => f
 bt


   | Typ _
 => f
 (bT
 (Typ_1 c
))

   | Knd _
 => f
 (bK
 (Knd_1 c
))

   end
.

simple
 destruct
 c
; auto
.

Qed
.




  Fixpoint
 cl_term (t
 : term) (i
 : cls) {struct
 t
} : class :=

    match
 t
 with


    | Srt _
 => Knd PROP

    | Ref n
 => match
 i
 n
 with


               | Knd s
 => Typ s


               | _
 => Trm

               end


    | Abs A
 B
 =>

        let
 clA
 := cl_term A
 i
 in


        match
 cl_term B
 (cons_map clA
 i
), clA
 with


        | Typ s2
, Knd s1
 => Typ (PROD s1
 s2
)

        | Typ s
, _
 => Typ s


        | Knd _
, _
 => Knd PROP

        | Trm, _
 => Trm

        end


    | App u
 v
 =>

        match
 cl_term u
 i
, cl_term v
 i
 with


        | Typ (PROD s1
 s2
), Typ s
 => Typ s2


        | Typ s
, _
 => Typ s


        | Knd _
, _
 => Knd PROP

        | Trm, _
 => Trm

        end


    | Prod T
 U
 =>

        let
 clT
 := cl_term T
 i
 in


        match
 cl_term U
 (cons_map clT
 i
), clT
 with


        | Knd s2
, Knd s1
 => Knd (PROD s1
 s2
)

        | Knd s
, _
 => Knd s


        | Typ s
, _
 => Typ s


        | c1
, _
 => c1


        end


    end
.




  Fixpoint
 class_env (e
 : env
) : cls :=

    match
 e
 with


    | nil => nil_cls

    | t
 :: f
 => cons_map (cl_term t
 (class_env f
)) (class_env f
)

    end
.




  Lemma
 cl_term_ext : forall
 t
 f
 g
, eq_map f
 g
 -> cl_term t
 f
 = cl_term t
 g
.

Proof
.

induction
 t
; simpl
; intros
; auto
.

rewrite
 H
; trivial
.




rewrite
 IHt1
 with
 (g
:=g); trivial
.

rewrite
 IHt2
 with
 (g
:=cons_map (cl_term t1
 g
) g
); auto
; intros
.




rewrite
 IHt1
 with
 (g
:=g); trivial
.

rewrite
 IHt2
 with
 (g
:=g); trivial
.




rewrite
 IHt1
 with
 (g
:=g); trivial
.

rewrite
 IHt2
 with
 (g
:=cons_map (cl_term t1
 g
) g
); auto
; intros
.

Qed
.




  Hint
 Resolve
 cl_term_ext : coc
.




  Lemma
 nth_class_env :

   forall
 t
 e
 n
,

   item t
 (e
:env) n
 ->

   class_env e
 n
 = cl_term t
 (del_map (S n
) 0 (class_env e
)).

Proof
.

simple
 induction
 1; simpl
 in
 |- *; intros
; auto
.

apply
 cl_term_ext; red
; auto
 with
 coc
.

Qed
.




  Lemma
 nth_class_env' :

   forall
 t
 e
 f
 n
,

   item t
 (e
:env) n
 ->

   trunc (S n
) e
 (f
:env) ->

   class_env e
 n
 = cl_term t
 (class_env f
).

Proof
.

simple
 induction
 1; simpl
 in
 |- *; intros
.

inversion_clear
 H0
.

inversion_clear
 H1
; auto
.




apply
 H1
.

inversion_clear
 H2
; auto
.

Qed
.




  Lemma
 class_knd :

   forall
 e
 t
 T
,

   typ e
 t
 T
 ->

   T
 = Srt kind ->

   cl_term t
 (class_env e
) = Knd (Knd_1 (cl_term t
 (class_env e
))).

Proof
.

simple
 induction
 1; intros
.

simpl
 in
 |- *; auto
 with
 coc
.




elim
 H1
; intros
.

elim
 item_trunc with
 term v
 e0
 x
; auto
 with
 coc
; intros
.

elim
 wf_sort with
 v
 e0
 x0
 x
; auto
 with
 coc
; intros
.

elim
 inv_typ_kind with
 e0
 (Srt x1
).

elim
 H2
.

rewrite
 H3
.

replace
 (Srt x1
) with
 (lift (S v
) (Srt x1
)); auto
 with
 coc
.

apply
 thinning_n with
 x0
; auto
 with
 coc
.




discriminate
 H6
.




elim
 type_case with
 (1 := H2
); intros
.

inversion_clear
 H5
.

apply
 inv_typ_prod with
 (1 := H6
); intros
.

elim
 inv_typ_kind with
 e0
 (Srt s2
); auto
 with
 coc
.

elim
 H4
.

replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




discriminate
 H5
.




simpl
 in
 H3
.

simpl
 in
 |- *.

rewrite
 H3
; auto
 with
 coc
.

elim
 (cl_term T0
 (class_env e0
)); auto
 with
 coc
.




elim
 inv_typ_kind with
 e0
 (Srt s
); auto
 with
 coc
.

elim
 H5
; auto
 with
 coc
.

Qed
.




  Lemma
 class_typ :

   forall
 e
 t
 T
,

   typ e
 t
 T
 ->

   typ e
 T
 (Srt kind) ->

   cl_term t
 (class_env e
) = Typ (Typ_1 (cl_term t
 (class_env e
))).

Proof
.

simple
 induction
 1; intros
.

elim
 inv_typ_kind with
 e0
 (Srt kind); trivial
.




elim
 H1
; intros
.

simpl
 in
 |- *.

elim
 item_trunc with
 term v
 e0
 x
; auto
 with
 coc
; intros
.

rewrite
 nth_class_env' with
 x
 e0
 x0
 v
; auto
 with
 coc
.

rewrite
 (class_knd x0
 x
 (Srt kind)); trivial
.

elim
 wf_sort with
 (1 := H5
) (3 := H4
); trivial
.

simple
 destruct
 x1
; trivial
; intros
.

absurd
 (kind = prop).

discriminate
.




apply
 conv_sort.

apply
 typ_unique with
 (1 := H2
).

rewrite
 H3
.

fold
 (lift_rec (S v
) (Srt prop) 0) (lift (S v
) (Srt prop)) in
 |- *.

apply
 thinning_n with
 (2 := H6
); trivial
.




simpl
 in
 |- *.

simpl
 in
 H5
.

rewrite
 H5
.

elim
 (cl_term T0
 (class_env e0
)); intros
; auto
 with
 coc
.




apply
 inv_typ_prod with
 (1 := H6
); intros
.

elim
 conv_sort with
 s3
 kind; auto
 with
 coc
.




simpl
 in
 |- *.

elim
 type_case with
 (1 := H2
); intros
.

inversion_clear
 H5
.

rewrite
 H3
.

case
 (Typ_1 (cl_term u
 (class_env e0
))); auto
 with
 coc
.




elim
 (cl_term v
 (class_env e0
)); auto
 with
 coc
.




apply
 inv_typ_prod with
 (1 := H6
); intros
.

apply
 type_prod with
 s1
; auto
 with
 coc
.

elim
 conv_sort with
 s2
 kind; auto
 with
 coc
.

apply
 typ_unique with
 e0
 (subst v
 Ur
); auto
 with
 coc
.

replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




discriminate
 H5
.




simpl
 in
 |- *.

simpl
 in
 H3
.

rewrite
 H3
; auto
 with
 coc
.

replace
 (Srt s2
) with
 (lift 1 (Srt s2
)); auto
 with
 coc
.

replace
 (Srt kind) with
 (lift 1 (Srt kind)); auto
 with
 coc
.

apply
 thinning; auto
 with
 coc
.

apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 H1
.

elim
 type_case with
 (1 := H0
); intros
.

inversion_clear
 H6
.

elim
 conv_sort with
 x
 kind; auto
 with
 coc
.

apply
 typ_conv_conv with
 e0
 U
 V
; auto
 with
 coc
.




elim
 inv_typ_conv_kind with
 e0
 V
 (Srt kind); auto
 with
 coc
.

elim
 H6
; auto
 with
 coc
.

Qed
.




  Lemma
 class_trm :

   forall
 e
 t
 T
,

   typ e
 t
 T
 -> typ e
 T
 (Srt prop) -> cl_term t
 (class_env e
) = Trm.

Proof
.

simple
 induction
 1; intros
.

elim
 inv_typ_kind with
 e0
 (Srt prop); auto
 with
 coc
.




elim
 H1
; intros
.

elim
 item_trunc with
 term v
 e0
 x
; auto
 with
 coc
; intros
.

elim
 wf_sort with
 (1 := H5
) (3 := H4
); trivial
.

simple
 destruct
 x1
; intros
.

absurd
 (kind = prop).

discriminate
.




apply
 conv_sort.

apply
 typ_unique with
 (2 := H2
).

rewrite
 H3
.

fold
 (lift_rec (S v
) (Srt kind) 0) (lift (S v
) (Srt kind)) in
 |- *.

apply
 thinning_n with
 (2 := H6
); trivial
.




simpl
 in
 |- *.

rewrite
 nth_class_env' with
 x
 e0
 x0
 v
; auto
 with
 coc
.

rewrite
 (class_typ x0
 x
 (Srt prop)); trivial
.

constructor
; prolog
 [ typ_wf ] 5.




simpl
 in
 |- *.

simpl
 in
 H5
.

rewrite
 H5
; auto
 with
 coc
.

apply
 inv_typ_prod with
 e0
 T0
 U
 (Srt prop); intros
; auto
 with
 coc
.

elim
 conv_sort with
 s3
 prop; auto
 with
 coc
.




simpl
 in
 |- *.

elim
 type_case with
 e0
 u
 (Prod V
 Ur
); auto
 with
 coc
; intros
.

inversion_clear
 H5
.

rewrite
 H3
; auto
 with
 coc
.

apply
 inv_typ_prod with
 e0
 V
 Ur
 (Srt x
); intros
; auto
 with
 coc
.

apply
 type_prod with
 s1
; auto
 with
 coc
.

elim
 conv_sort with
 s2
 prop; auto
 with
 coc
.

apply
 typ_unique with
 e0
 (subst v
 Ur
); auto
 with
 coc
.

replace
 (Srt s2
) with
 (subst v
 (Srt s2
)); auto
 with
 coc
.

apply
 substitution with
 V
; auto
 with
 coc
.




discriminate
 H5
.




simpl
 in
 |- *.

simpl
 in
 H3
.

rewrite
 H3
; auto
 with
 coc
.

replace
 (Srt s2
) with
 (lift 1 (Srt s2
)); auto
 with
 coc
.

replace
 (Srt prop) with
 (lift 1 (Srt prop)); auto
 with
 coc
.

apply
 thinning; auto
 with
 coc
.

apply
 wf_var with
 s1
; auto
 with
 coc
.




apply
 H1
.

elim
 type_case with
 e0
 t0
 U
; auto
 with
 coc
; intros
.

inversion_clear
 H6
.

elim
 conv_sort with
 x
 prop; auto
 with
 coc
.

apply
 typ_conv_conv with
 e0
 U
 V
; auto
 with
 coc
.




elim
 inv_typ_conv_kind with
 e0
 V
 (Srt prop); auto
 with
 coc
.

elim
 H6
; auto
 with
 coc
.

Qed
.




  Inductive
 adj_cls : class -> class -> Prop
 :=

    | adj_t : forall
 s
, adj_cls Trm (Typ s
)

    | adj_T : forall
 s1
 s2
, adj_cls (Typ s1
) (Knd s2
).




  Hint
 Constructors
 adj_cls
: coc
.




  Lemma
 cl_term_sound :

   forall
 e
 t
 T
 K
,

   typ e
 t
 T
 ->

   typ e
 T
 K
 -> adj_cls (cl_term t
 (class_env e
)) (cl_term T
 (class_env e
)).

Proof
.

intros
.

elim
 type_case with
 (1 := H
); intros
; auto
 with
 coc
.

elim
 H1
.

simple
 destruct
 x
; intros
.

rewrite
 (class_knd e
 T
 (Srt kind)); auto
 with
 coc
.

rewrite
 (class_typ e
 t
 T
); auto
 with
 coc
.




rewrite
 (class_typ e
 T
 (Srt prop)); auto
 with
 coc
.

rewrite
 (class_trm e
 t
 T
); auto
 with
 coc
.




apply
 type_prop.

apply
 typ_wf with
 t
 T
; auto
 with
 coc
.




elim
 inv_typ_kind with
 e
 K
; auto
 with
 coc
.

elim
 H1
; auto
 with
 coc
.

Qed
.




  Lemma
 class_lift :

   forall
 n
 t
 k
 f
, cl_term (lift_rec n
 t
 k
) f
 = cl_term t
 (del_map n
 k
 f
).

simple
 induction
 t
; intros
.

simpl
 in
 |- *; auto
.




simpl
 in
 |- *.

unfold
 del_map
.

elim
 (le_gt_dec k
 n0
); simpl
 in
 |- *; trivial
.




simpl
 in
 |- *.

rewrite
 H
; rewrite
 H0
.

rewrite
 cl_term_ext with
 

 (g
:=cons_map (cl_term t0
 (del_map n
 k
 f
)) (del_map n
 k
 f
)).

2:apply del_cons_map.

trivial
.




simpl
 in
 |- *.

rewrite
 H
; rewrite
 H0
.

trivial
.




simpl
 in
 *.

rewrite
 H
; rewrite
 H0
.

rewrite
 cl_term_ext with
 

 (g
:=cons_map (cl_term t0
 (del_map n
 k
 f
)) (del_map n
 k
 f
)).

2:apply del_cons_map.

trivial
.

Qed
.







  Inductive
 typ_cls : class -> class -> Prop
 :=

    | tc_t : typ_cls Trm (Typ PROP)

    | tc_T : forall
 s
, typ_cls (Typ s
) (Knd s
).




  Hint
 Constructors
 typ_cls
: coc
.




  Lemma
 class_subst :

   forall
 a
 x
 t
 k
 E
,

   typ_cls (cl_term x
 (del_map k
 0 E
)) a
 ->

   cl_term (subst_rec x
 t
 k
) E
 = cl_term t
 (ins_map k
 a
 E
).

simple
 induction
 t
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

unfold
 ins_map
.




elim
 (lt_eq_lt_dec k
 n
); simpl
 in
 |- *; intros
; auto
.

elim
 a0
; intros
; auto
.

unfold
 lift
; rewrite
 class_lift.

elim
 H
; trivial
.




rewrite
 H
 with
 (1:=H1).

rewrite
 H0
 with
 (S k
) (cons_map (cl_term t0
 (ins_map k
 a
 E
)) E
).

rewrite
 cl_term_ext with


  (g
:=cons_map (cl_term t0
 (ins_map k
 a
 E
)) (ins_map k
 a
 E
)).

trivial
.

apply
 ins_cons_map.




exact
 H1
.




rewrite
 H
 with
 (1:=H1).

rewrite
 H0
 with
 (1:=H1).

trivial
.




rewrite
 H
 with
 (1:=H1).

rewrite
 H0
 with
 (S k
) (cons_map (cl_term t0
 (ins_map k
 a
 E
)) E
).

rewrite
 cl_term_ext with


  (g
:=cons_map (cl_term t0
 (ins_map k
 a
 E
)) (ins_map k
 a
 E
)).

trivial
.

apply
 ins_cons_map.




exact
 H1
.

Qed
.







  Inductive
 loose_eqc : class -> class -> Prop
 :=

    | leqc_trm : loose_eqc Trm Trm

    | leqc_typ : forall
 s1
 s2
, loose_eqc (Typ s1
) (Typ s2
)

    | leqc_ord : forall
 s
, loose_eqc (Knd s
) (Knd s
).




  Hint
 Constructors
 loose_eqc
: coc
.




  Lemma
 refl_loose_eqc : forall
 c
, loose_eqc c
 c
.

Proof
.

simple
 destruct
 c
; constructor
.

Qed
.




  Hint
 Resolve
 refl_loose_eqc: coc
.




  Lemma
 loose_eqc_trans :

   forall
 c1
 c2
,

   loose_eqc c1
 c2
 -> forall
 c3
, loose_eqc c2
 c3
 -> loose_eqc c1
 c3
.

Proof
.

simple
 destruct
 1; intros
; inversion_clear
 H0
; auto
 with
 coc
.

Qed
.




  Lemma
 loose_eqc_stable :

   forall
 t
 cl1
 cl2
,

   (forall
 n
, loose_eqc (cl1
 n
) (cl2
 n
)) ->

   loose_eqc (cl_term t
 cl1
) (cl_term t
 cl2
).

Proof
.

simple
 induction
 t
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

elim
 (H
 n
); auto
 with
 coc
.




case
 H0
 with
 

 (cons_map (cl_term t0
 cl1
) cl1
) (cons_map (cl_term t0
 cl2
) cl2
);

 auto
 with
 coc
.

destruct
 n
; simpl
; auto
.




case
 H
 with
 (1 := H1
); auto
 with
 coc
; intros
.




case
 H
 with
 (1 := H1
); auto
 with
 coc
; intros
.

case
 s1
; case
 s2
; case
 H0
 with
 (1 := H1
); auto
 with
 coc
; intros
.




case
 H0
 with
 

 (cons_map (cl_term t0
 cl1
) cl1
) (cons_map (cl_term t0
 cl2
) cl2
);

 auto
 with
 coc
.

destruct
 n
; simpl
; auto
.




case
 H
 with
 (1 := H1
); auto
 with
 coc
; intros
.

Qed
.




  Hint
 Resolve
 loose_eqc_stable: coc
.




  Lemma
 cl_term_subst :

   forall
 a
 x
 t
 k
 E
,

   adj_cls (cl_term x
 (del_map k
 0 E
)) a
 ->

   loose_eqc (cl_term t
 (ins_map k
 a
 E
)) (cl_term (subst_rec x
 t
 k
) E
).

Proof
.

simple
 induction
 t
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

unfold
 ins_map
.

generalize
 (lt_eq_lt_dec k
 n
); intros
 [[H0
|H0]|H0]; simpl
 in
 |- *; auto
 with
 coc
.

unfold
 lift
; rewrite
 class_lift.

elim
 H
; auto
 with
 coc
.




assert
 (loose_eqc (cl_term t0
 (ins_map k
 a
 E
)) (cl_term (subst_rec x
 t0
 k
) E
)); intros
;

 auto
 with
 coc
.

assert


 (loose_eqc

   (cl_term t1
 (cons_map (cl_term t0
 (ins_map k
 a
 E
)) (ins_map k
 a
 E
)))

   (cl_term (subst_rec x
 t1
 (S k
)) (cons_map (cl_term (subst_rec x
 t0
 k
) E
) E
)));

 intros
.

apply


 loose_eqc_trans with


   (cl_term t1
 (cons_map (cl_term (subst_rec x
 t0
 k
) E
) (ins_map k
 a
 E
)));

 auto
 with
 coc
.

apply
 loose_eqc_stable.

destruct
 n
; simpl
; auto
 with
 coc
.




rewrite
 <- cl_term_ext with


  (f
:=ins_map (S k
) a
 (cons_map (cl_term (subst_rec x
 t0
 k
) E
) E
)).

auto
 with
 coc
.

apply
 ins_cons_map.




elim
 H3
; auto
 with
 coc
; intros
.

elim
 H2
; auto
 with
 coc
.




elim
 H
 with
 k
 E
; auto
 with
 coc
; intros
.

elim
 s1
; elim
 s2
; elim
 H0
 with
 k
 E
; auto
 with
 coc
.




assert
 (loose_eqc (cl_term t0
 (ins_map k
 a
 E
)) (cl_term (subst_rec x
 t0
 k
) E
)); intros
;

 auto
 with
 coc
.

assert


 (loose_eqc (cl_term t1
 (cons_map (cl_term t0
 (ins_map k
 a
 E
)) (ins_map k
 a
 E
)))

    (cl_term (subst_rec x
 t1
 (S k
)) (cons_map (cl_term (subst_rec x
 t0
 k
) E
) E
)));

 intros
.

apply


 loose_eqc_trans with


   (cl_term t1
 (cons_map (cl_term (subst_rec x
 t0
 k
) E
) (ins_map k
 a
 E
)));

 auto
 with
 coc
.

apply
 loose_eqc_stable.

destruct
 n
; simpl
; auto
 with
 coc
.




rewrite
 <- cl_term_ext with


  (f
:=ins_map (S k
) a
 (cons_map (cl_term (subst_rec x
 t0
 k
) E
) E
)).

auto
 with
 coc
.

apply
 ins_cons_map.




elim
 H3
; auto
 with
 coc
; intros
.

elim
 H2
; auto
 with
 coc
.

Qed
.




 Lemma
 cl_term_subst0 :

   forall
 a
 x
 t
 E
,

   adj_cls (cl_term x
 E
) a
 ->

   loose_eqc (cl_term t
 (cons_map a
 E
)) (cl_term (subst x
 t
) E
).

Proof
.

intros
.

rewrite
 cl_term_ext with
 (g
:=ins_map 0 a
 E
).

unfold
 subst
.

apply
 cl_term_subst.

rewrite
 cl_term_ext with
 (g
:=E); try
 red
; auto
 with
 coc
.




red
; destruct
 i
; auto
 with
 coc
.

Qed
.




  Lemma
 cl_term_red1 :

   forall
 e
 A
 T
,

   typ e
 A
 T
 ->

   forall
 B
,

   red1 A
 B
 -> loose_eqc (cl_term A
 (class_env e
)) (cl_term B
 (class_env e
)).

simple
 induction
 1; intros
; auto
 with
 coc
.

inversion_clear
 H1
.




inversion_clear
 H2
.




inversion_clear
 H6
.

simpl
 in
 |- *.

elim
 loose_eqc_stable

  with
 M
 (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
))

    (cons_map (cl_term M'
 (class_env e0
)) (class_env e0
)); 

 auto
 with
 coc
.

elim
 H1
 with
 M'
; auto
 with
 coc
.

destruct
 n
 ; simpl
; auto
 with
 coc
.




simpl
.

change
 (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
)) with


 (class_env (T0
 :: e0
)).

elim
 H5
 with
 M'
; auto
 with
 coc
.

elim
 (cl_term T0
 (class_env e0
)); auto
 with
 coc
.




generalize
 H2
 H3
; clear
 H2
 H3
.

inversion_clear
 H4
; intros
.

elim
 type_case with
 (1 := H2
); intros
.

inversion_clear
 H4
.

apply
 inv_typ_prod with
 (1 := H5
); intros
.

apply
 inv_typ_abs with
 (1 := H2
); intros
.

simpl
 in
 |- *.

apply
 loose_eqc_trans with
 (cl_term M
 (class_env (T0
 :: e0
))).

unfold
 class_env
 in
 |- *; fold
 (class_env (T0
 :: e0
)) class_env in
 |- *;

 auto
 with
 coc
.

elim
 cl_term_sound with
 (1 := H9
) (2 := H10
); intros
; auto
 with
 coc
.

elim
 (cl_term T0
 (class_env e0
)); intros
.

elim
 s4
; elim
 (cl_term v
 (class_env e0
)); auto
 with
 coc
.




elim
 s4
; elim
 (cl_term v
 (class_env e0
)); auto
 with
 coc
.




elim
 (cl_term v
 (class_env e0
)); auto
 with
 coc
.




simpl
.

apply
 cl_term_subst0.

apply
 cl_term_sound with
 (Srt s0
); auto
 with
 coc
.

apply
 type_conv with
 V
 s0
; auto
 with
 coc
.

apply
 inv_conv_prod_l with
 Ur
 T1
; auto
 with
 coc
.




discriminate
.




simpl
 in
 |- *.

elim
 H4
 with
 N1
; intros
; auto
 with
 coc
.

case
 s1
; case
 s2
; elim
 (cl_term v
 (class_env e0
)); auto
 with
 coc
.




simpl
 in
 |- *.

elim
 (cl_term u
 (class_env e0
)); intros
; auto
 with
 coc
.

case
 s
; elim
 H1
 with
 N2
; auto
 with
 coc
.




inversion_clear
 H4
.

simpl
 in
 |- *.

elim
 loose_eqc_stable

  with


    U


    (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
))

    (cons_map (cl_term N1
 (class_env e0
)) (class_env e0
)); 

 auto
 with
 coc
.

elim
 H1
 with
 N1
; auto
 with
 coc
.

destruct
 n
; simpl
; auto
 with
 coc
.




simpl
 in
 |- *.

unfold
 class_env
 in
 |- *; fold
 (class_env (T0
 :: e0
)) class_env in
 |- *;

 auto
 with
 coc
.

elim
 H3
 with
 N2
; auto
 with
 coc
.

Qed
.




  Lemma
 cl_term_red :

   forall
 T
 U
,

   red T
 U
 ->

   forall
 e
 K
,

   typ e
 T
 K
 -> loose_eqc (cl_term T
 (class_env e
)) (cl_term U
 (class_env e
)).

Proof
.

simple
 induction
 1; intros
; auto
 with
 coc
.

apply
 loose_eqc_trans with
 (cl_term P
 (class_env e
)); auto
 with
 coc
.

apply
 H1
 with
 K
; auto
 with
 coc
.




apply
 cl_term_red1 with
 K
; auto
 with
 coc
.

apply
 subject_reduction with
 T
; auto
 with
 coc
.

Qed
.




  Lemma
 cl_term_conv :

   forall
 e
 T
 U
 K1
 K2
,

   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
)).

Proof
.

intros
.

elim
 church_rosser with
 (1 := H1
); intros
.

apply
 loose_eqc_trans with
 (cl_term x
 (class_env e
)).

apply
 cl_term_red with
 K1
; auto
 with
 coc
.




elim
 cl_term_red with
 U
 x
 e
 K2
; auto
 with
 coc
.

Qed
.




  Lemma
 skel_sound :

   forall
 e
 t
 T
,

   typ e
 t
 T
 ->

   Knd_1 (cl_term T
 (class_env e
)) = Typ_1 (cl_term t
 (class_env e
)).

Proof
.

simple
 induction
 1; intros
; auto
 with
 coc
.

inversion_clear
 H1
.

subst
 t0
.

unfold
 lift
.

rewrite
 class_lift.

unfold
 del_map
.

simpl
.

elim
 H3
; simpl
 in
 |- *; intros
; auto
.

rewrite
 cl_term_ext with
 (g
:=class_env l
); try
 red
; auto
.

case
 (cl_term x
 (class_env l
)); simpl
; auto
.




simpl
 in
 |- *.

unfold
 class_env
 in
 |- *; fold
 (class_env (T0
 :: e0
)) class_env in
 |- *;

 auto
 with
 coc
.

rewrite


 (commut_case _
 _
 Knd_1 (cl_term U
 (class_env (T0
 :: e0
)))

    (cl_term U
 (class_env (T0
 :: e0
))) (fun
 s
 => Typ s
)

    (fun
 s
 =>

     match
 cl_term T0
 (class_env e0
) with


     | Trm => Knd s


     | Typ _
 => Knd s


     | Knd s0
 => Knd (PROD s0
 s
)

     end
)).

rewrite


 (commut_case _
 _
 Typ_1 (cl_term M
 (class_env (T0
 :: e0
))) Trm

    (fun
 s
 =>

     match
 cl_term T0
 (class_env e0
) with


     | Trm => Typ s


     | Typ _
 => Typ s


     | Knd s0
 => Typ (PROD s0
 s
)

     end
) (fun
 _
 => Knd PROP)).

pattern
 (cl_term M
 (class_env (T0
 :: e0
))) at
 1,

 (cl_term U
 (class_env (T0
 :: e0
))) at
 1 in
 |- *.

elim
 cl_term_sound with
 (1 := H4
) (2 := H2
); intros
; auto
 with
 coc
.

rewrite


 (commut_case _
 _
 Knd_1 (cl_term T0
 (class_env e0
))

    (Knd (Knd_1 (cl_term U
 (class_env (T0
 :: e0
)))))

    (fun
 _
 => Knd (Knd_1 (cl_term U
 (class_env (T0
 :: e0
)))))

    (fun
 s4
 => Knd (PROD s4
 (Knd_1 (cl_term U
 (class_env (T0
 :: e0
)))))))

 .

elim
 (cl_term T0
 (class_env e0
)); simpl
 in
 |- *; auto
 with
 coc
.

unfold
 class_env
 in
 |- *; fold
 (class_env (T0
 :: e0
)) class_env in
 |- *;

 auto
 with
 coc
.

elim
 H5
; auto
 with
 coc
.




elim
 type_case with
 (1 := H2
); intros
.

inversion_clear
 H4
.

apply
 inv_typ_prod with
 (1 := H5
); intros
.

assert
 (adj_cls (cl_term u
 (class_env e0
)) (cl_term (Prod V
 Ur
) (class_env e0
))).

apply
 cl_term_sound with
 (Srt x
); auto
 with
 coc
.




generalize
 H3
 H8
; clear
 H3
 H8
.

simpl
 in
 |- *.

elim
 cl_term_subst0

  with
 (cl_term V
 (class_env e0
)) v
 Ur
 (class_env e0
);

 simpl
 in
 |- *; auto
 with
 coc
.

intros
.

inversion_clear
 H8
.




intros
.

inversion_clear
 H8
.

auto
 with
 coc
.




elim
 cl_term_sound with
 e0
 v
 V
 (Srt s1
); simpl
 in
 |- *; intros
; auto
 with
 coc
.

rewrite
 H3
.

inversion_clear
 H8
; auto
 with
 coc
.

case
 s3
; auto
 with
 coc
.




generalize
 H3
.

inversion_clear
 H8
; intros
; auto
 with
 coc
.

simpl
 in
 H8
.

elim
 H8
; auto
 with
 coc
.




apply
 cl_term_sound with
 (Srt s1
); auto
 with
 coc
.




discriminate
 H4
.




simpl
 in
 |- *.

simpl
 in
 H3
.

simpl
 in
 H1
.

rewrite


 (commut_case _
 _
 Typ_1

    (cl_term U
 (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
)))

    (cl_term U
 (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
)))

    (fun
 s
 => Typ s
)

    (fun
 s
 =>

     match
 cl_term T0
 (class_env e0
) with


     | Trm => Knd s


     | Typ _
 => Knd s


     | Knd s0
 => Knd (PROD s0
 s
)

     end
)).

simpl
 in
 |- *.

elim
 H3
.

elim
 (cl_term U
 (cons_map (cl_term T0
 (class_env e0
)) (class_env e0
)));

 auto
 with
 coc
.

elim
 (cl_term T0
 (class_env e0
)); auto
 with
 coc
.




elim
 H1
.

elim
 cl_term_conv with
 e0
 U
 V
 (Srt s
) (Srt s
); auto
 with
 coc
.

elim
 type_case with
 e0
 t0
 U
; auto
 with
 coc
; intros
.

inversion_clear
 H5
.

elim
 conv_sort with
 x
 s
; auto
 with
 coc
.

apply
 typ_conv_conv with
 e0
 U
 V
; auto
 with
 coc
.




elim
 inv_typ_conv_kind with
 e0
 V
 (Srt s
); auto
 with
 coc
.

elim
 H5
; auto
 with
 coc
.

Qed
.







  Lemma
 class_red :

   forall
 e
 T
 U
 K
,

   typ e
 T
 K
 -> red T
 U
 -> cl_term T
 (class_env e
) = cl_term U
 (class_env e
).

Proof
.

intros
.

cut
 (Typ_1 (cl_term T
 (class_env e
)) = Typ_1 (cl_term U
 (class_env e
))).

elim
 cl_term_red with
 T
 U
 e
 K
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

elim
 H1
; auto
 with
 coc
.




elim
 skel_sound with
 (1 := H
); auto
 with
 coc
.

apply
 skel_sound; auto
 with
 coc
.

apply
 subject_reduction with
 T
; auto
 with
 coc
.

Qed
.




  Lemma
 class_sound :

   forall
 e
 t
 T
 K
,

   typ e
 t
 T
 ->

   typ e
 T
 K
 -> typ_cls (cl_term t
 (class_env e
)) (cl_term T
 (class_env e
)).

Proof
.

intros
.

elim
 type_case with
 (1 := H
); intros
.

elim
 H1
.

simple
 destruct
 x
; intros
.

rewrite
 (class_knd e
 T
 (Srt kind)); trivial
.

rewrite
 (class_typ e
 t
 T
); trivial
.

elim
 skel_sound with
 (1 := H
); auto
 with
 coc
.




rewrite
 (class_typ e
 T
 (Srt prop)); trivial
.

rewrite
 (class_trm e
 t
 T
); trivial
.

elim
 skel_sound with
 (1 := H2
); simpl
 in
 |- *; auto
 with
 coc
.




apply
 type_prop.

apply
 typ_wf with
 t
 T
; auto
 with
 coc
.




elim
 inv_typ_kind with
 e
 K
.

elim
 H1
; auto
 with
 coc
.

Qed
.




Lemma
 class_type: forall
 e
 t
 s
 (P
:class->Prop),

  typ e
 t
 (Srt s
) ->

  (cl_term t
 (class_env e
) = Typ PROP -> P
 (Typ PROP)) ->

  (forall
 s
, cl_term t
 (class_env e
) = Knd s
 -> P
 (Knd s
)) ->

  P
 (cl_term t
 (class_env e
)).

Proof
.

destruct
 s
; intros
.

generalize
 H1
.

rewrite
 class_knd with
 (1:= H
); auto
.




generalize
 H0
.

rewrite
 class_typ with
 (1:=H); trivial
.

assert
 (Knd_1 (cl_term (Srt prop) (class_env e
)) = PROP). reflexivity
.

generalize
 H2
; clear
 H2
.

elim
 class_sound with
 (1:=H) (K
:=Srt kind); simpl
; intros
; auto
.

subst
 s
; auto
.

constructor
; eapply
 typ_wf; eauto
.




constructor
; eapply
 typ_wf; eauto
.

Qed
.




Lemma
 class_term: forall
 e
 t
 T
 s
 (P
:class->class->Prop),

  typ e
 t
 T
 ->

  typ e
 T
 (Srt s
) ->

  (cl_term t
 (class_env e
) = Trm ->

  cl_term T
 (class_env e
) = Typ PROP ->

  P
 Trm (Typ PROP)) ->

  (forall
 s
, cl_term t
 (class_env e
) = Typ s
 ->

   cl_term T
 (class_env e
) = Knd s
 ->

   P
 (Typ s
) (Knd s
)) ->

  P
 (cl_term t
 (class_env e
)) (cl_term T
 (class_env e
)).

Proof
.

intros
.

specialize
 class_sound with
 (1:=H) (2:=H0).

apply
 class_type with
 (1:=H0); intros
.

generalize
 H1
.

inversion_clear
 H4
; auto
.




generalize
 H2
.

inversion_clear
 H4
; auto
.

Qed
.