proposition: Lemma Ered_Econv : forall M N : term, Ered M N -> Econv M N.
proof: Proof. simple induction 1; auto with ecoc coc core arith sets. intros; apply Etrans_conv_red with P; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv