proposition: Theorem Econv_church_rosser : forall u v : term, Econv u v -> ex2 (fun t : term => Ered u t) (fun t : term => Ered v t).
proof: Proof. simple induction 1; intros. exists u; auto with ecoc coc core arith sets. elim H1; intros. elim confluence_Ered with x P N; auto with ecoc coc core arith sets; intros. exists x0; auto with ecoc coc core arith sets. apply trans_Ered_Ered with x; auto with ecoc coc core arith sets. elim H1; intros. exists x; auto with ecoc coc core arith sets. apply trans_Ered_Ered with P; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv