proposition: Theorem Strip : forall (U : Type) (R : Relation U), Strongly_confluent R -> forall x b : U, Rstar R x b -> forall a : U, R x a -> exists z : U, Rstar 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. intros x0 y z H'1 H'2 H'3 a H'4. red in H'. generalize (H' x0 a y); intro h; lapply h; [ intro H'5; lapply H'5; [ intro h0; elim h0; intros t h1; elim h1; intros H'6 H'7; clear h H'5 h0 h1; try exact H'6 | clear h ] | clear h ]; auto 10. generalize (H'3 t); intro h; lapply h; [ intro h0; elim h0; intros z1 h1; elim h1; intros H'5 H'8; clear h h0 h1; try exact H'5 | clear h ]; auto 10. exists z1; split; [ idtac | assumption ]. apply Rstar_n with t; auto. Qed.
imports: Relations Confluence Coherence