proposition: Lemma class_trm : forall (e : env) (t T : term) (s : sort), is_prop s -> typ e t T -> typ e T (Srt s) -> cl_term t (class_env e) = Trm.
proof: Proof. intros e t T s is_p. simple induction 1; intros. elim inv_typ_kind with e0 (Srt s); auto with coc core arith datatypes. elim inv_typ_kind with e0 (Srt s); auto with coc core arith datatypes. elim H1; intros. simpl in |- *. elim item_trunc with term v e0 x; auto with coc core arith datatypes; intros. elim nth_class_env with x e0 x0 v; auto with coc core arith datatypes. elim cl_trunc with (S v) (class_env e0) (class_env x0) x; auto with coc core arith datatypes. elim H3. rewrite (class_typ e0 t0 (Srt s)); auto with coc core arith datatypes. apply type_prop_set; auto with coc core arith datatypes. simpl in |- *. simpl in H5. rewrite H5; auto with coc core arith datatypes. apply inv_typ_prod with e0 T0 U (Srt s); intros; auto with coc core arith datatypes. elim conv_sort with s3 s; auto with coc core arith datatypes. simpl in |- *. elim type_case with e0 u (Prod V Ur); auto with coc core arith datatypes; intros. inversion_clear H5. rewrite H3; auto with coc core arith datatypes. apply inv_typ_prod with e0 V Ur (Srt x); intros; auto with coc core arith datatypes. apply type_prod with s1; auto with coc core arith datatypes. elim conv_sort with s2 s; auto with coc core arith datatypes. apply typ_unique with e0 (subst v Ur); auto with coc core arith datatypes. replace (Srt s2) with (subst v (Srt s2)); auto with coc core arith datatypes. apply substitution with V; auto with coc core arith datatypes. discriminate H5. simpl in |- *. simpl in H3. rewrite H3; auto with coc core arith datatypes. replace (Srt s2) with (lift 1 (Srt s2)); auto with coc core arith datatypes. replace (Srt s) with (lift 1 (Srt s)); auto with coc core arith datatypes. apply thinning; auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. apply H1. elim type_case with e0 t0 U; auto with coc core arith datatypes; intros. inversion_clear H6. elim conv_sort with x s; auto with coc core arith datatypes. apply typ_conv_conv with e0 U V; auto with coc core arith datatypes. elim inv_typ_conv_kind with e0 V (Srt s); auto with coc core arith datatypes. elim H6; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType