proposition: Lemma cl_term_sound : forall (e : env) (t T : term), typ e t T -> forall K : term, typ e T K -> adj_cls (cl_term t (class_env e)) (cl_term T (class_env e)).
proof: Proof. intros. elim type_case with e t T; intros; auto with coc core arith datatypes. elim H1. intro x; elim x using sort_level_ind; intros. rewrite (class_knd e T (Srt kind)); auto with coc core arith datatypes. rewrite (class_typ e t T); auto with coc core arith datatypes. rewrite (class_typ e T (Srt s)); auto with coc core arith datatypes. rewrite (class_trm e t T s); auto with coc core arith datatypes. apply type_prop_set; trivial. apply typ_wf with t T; auto with coc core arith datatypes. elim inv_typ_kind with e K; auto with coc core arith datatypes. elim H1; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType