proposition: Lemma loose_eqc_stable : forall (t : term) (cl1 cl2 : cls), Tfor_all2 _ _ loose_eqc cl1 cl2 -> loose_eqc (cl_term t cl1) (cl_term t cl2).
proof: Proof. simple induction t; simpl in |- *; intros; auto with coc core arith datatypes. generalize n. elim H; simpl in |- *; intros; auto with coc core arith datatypes. case n0; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. elim H0 with (TCs class (cl_term t0 cl1) cl1) (TCs class (cl_term t0 cl2) cl2); auto with coc core arith datatypes. elim H with cl1 cl2; auto with coc core arith datatypes. elim H with cl1 cl2; auto with coc core arith datatypes; intros. elim s1; elim s2; elim H0 with cl1 cl2; auto with coc core arith datatypes. elim H0 with (TCs class (cl_term t0 cl1) cl1) (TCs class (cl_term t0 cl2) cl2); auto with coc core arith datatypes. elim H with cl1 cl2; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types ListType