proposition: Lemma class_red : forall (e : env) (T U K : term), typ e T K -> red T U -> cl_term T (class_env e) = cl_term U (class_env e).
proof: Proof. intros. cut (typ_skel (cl_term T (class_env e)) = typ_skel (cl_term U (class_env e))). elim cl_term_red with (1 := H0) (2 := H); simpl in |- *; intros; trivial. elim H1; trivial. elim skel_sound with (1 := H); trivial. apply skel_sound. apply subject_reduction with (1 := H0) (2 := H). Qed.
imports: Termes Conv Types ListType