proposition: Lemma cl_term_conv : forall (e : env) (T U K1 K2 : term), 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: Proof. intros. elim church_rosser with T U; intros; auto with coc core arith datatypes. apply loose_eqc_trans with (cl_term x (class_env e)). apply cl_term_red with K1; auto with coc core arith datatypes. elim cl_term_red with U x e K2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType