proposition: Lemma Ered_Ered_app : forall u u0 v v0 : term, Ered u u0 -> Ered v v0 -> Ered (App u v) (App u0 v0).
proof: Proof. simple induction 1. simple induction 1; intros; auto with ecoc coc core arith sets. apply Etrans_red with (App u P); auto with ecoc coc core arith sets. intros; apply Etrans_red with (App P v0); auto with ecoc coc core arith sets. Qed.
imports: Termes Conv