proposition: Lemma class_sound : forall (e : env) (t T : term), typ e t T -> forall K : term, typ e T K -> typ_cls (cl_term t (class_env e)) (cl_term T (class_env e)).
proof: Proof. intros. elim type_case with (1 := H); intros. elim H1. intro x; elim x using sort_level_ind; 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 s)); trivial. rewrite (class_trm e t T s); trivial. elim skel_sound with (1 := H3); simpl in |- *; auto with coc. apply type_prop_set; trivial. apply typ_wf with t T; auto with coc. elim inv_typ_kind with e K. elim H1; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType