proposition: Lemma Epar_red_Ered : forall M N : term, Epar_red M N -> Ered M N.
proof: Proof. simple induction 1. simple induction 1; intros; eauto with ecoc coc core arith sets. intros; apply trans_Ered_Ered with y; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv