proposition: Lemma trans_Ered_Ered : forall M N P : term, Ered M N -> Ered N P -> Ered M P.
proof: Proof. intros. generalize H0 M H. simple induction 1; auto with ecoc coc core arith sets. intros; apply Etrans_red with P0; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv