proposition: Lemma Ered_Epar_red : forall M N : term, Ered M N -> Epar_red M N.
proof: Proof. red in |- *; simple induction 1; intros; auto with ecoc coc core arith sets. apply t_trans with P; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv