proposition: Lemma loose_eqc_trans : forall c1 c2 : class, loose_eqc c1 c2 -> forall c3 : class, loose_eqc c2 c3 -> loose_eqc c1 c3.
proof: Proof. simple induction 1; intros; inversion_clear H0; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType