proposition: Lemma cl_term_red : forall T U : term, red T U -> forall (e : env) (K : term), typ e T K -> loose_eqc (cl_term T (class_env e)) (cl_term U (class_env e)).
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. apply loose_eqc_trans with (cl_term P (class_env e)); auto with coc core arith datatypes. apply H1 with K; auto with coc core arith datatypes. apply cl_term_red1 with K; auto with coc core arith datatypes. apply subject_reduction with T; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType