proposition: Lemma class_typ_ord : forall (e : env) (T : term) (s : sort), typ e T (Srt s) -> forall P : class -> Prop, P (Typ (typ_skel (cl_term T (class_env e)))) -> P (Knd (cv_skel (cl_term T (class_env e)))) -> P (cl_term T (class_env e)).
proof: Proof. simple destruct s; intros. rewrite (class_knd e T (Srt kind)); auto with coc core arith datatypes. rewrite (class_typ e T (Srt prop)); auto with coc core arith datatypes. apply type_prop. apply typ_wf with T (Srt prop); auto with coc core arith datatypes. rewrite (class_typ e T (Srt set)); auto with coc core arith datatypes. apply type_set. apply typ_wf with T (Srt set); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType