proposition: Theorem church_rosser : forall u v, conv u v -> ex2 (fun t => red u t) (fun t => red v t).
proof: Proof. simple induction 1; intros. exists u; auto with coc core arith sets. elim H1; intros. elim confluence_red with x P N; auto with coc core arith sets; intros. exists x0; auto with coc core arith sets. apply trans_red_red with x; auto with coc core arith sets. elim H1; intros. exists x; auto with coc core arith sets. apply trans_red_red with P; auto with coc core arith sets. Qed.
imports: Termes