proposition: Theorem Lemma1 : forall (U:Type) (R:Relation U), Strongly_confluent U R -> forall x b:U, Rstar U R x b -> forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z.
proof: Proof. intros U R H' x b H'0; elim H'0. - intros x0 a H'1; exists a; auto with sets. - intros x0 y z H'1 H'2 H'3 a H'4. red in H'. specialize H' with (x := x0) (a := a) (b := y); lapply H'; [ intro H'8; lapply H'8; [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ] | clear H' ]; auto with sets. elim H'9. intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5. elim (H'3 t); auto with sets. intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. exists z1; split; [ idtac | assumption ]. apply Rstar_n with t; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2