Relations_2_facts.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Relations_2.

Theorem Rstar_reflexive :
 forall (U:Type) (R:Relation U), Reflexive U (Rstar U R).forall (U : Type) (R : Relation U),
Reflexive U (Rstar U R)
Proof.forall (U : Type) (R : Relation U),
Reflexive U (Rstar U R)
auto with sets.
Qed.

Theorem Rplus_contains_R :
 forall (U:Type) (R:Relation U), contains U (Rplus U R) R.forall (U : Type) (R : Relation U),
contains U (Rplus U R) R
Proof.forall (U : Type) (R : Relation U),
contains U (Rplus U R) R
auto with sets.
Qed.

Theorem Rstar_contains_R :
 forall (U:Type) (R:Relation U), contains U (Rstar U R) R.forall (U : Type) (R : Relation U),
contains U (Rstar U R) R
Proof.forall (U : Type) (R : Relation U),
contains U (Rstar U R) R
intros U R; red; intros x y H'; apply Rstar_n with y; auto with sets.
Qed.

Theorem Rstar_contains_Rplus :
 forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).forall (U : Type) (R : Relation U),
contains U (Rstar U R) (Rplus U R)
Proof.forall (U : Type) (R : Relation U),
contains U (Rstar U R) (Rplus U R)
intros U R; red.U:Type
R:Relation U
forall x y : U, Rplus U R x y -> Rstar U R x y
intros x y H'; elim H'.U:Type
R:Relation U
x, y:U
H':Rplus U R x y
forall x0 y0 : U, R x0 y0 -> Rstar U R x0 y0
U:Type
R:Relation U
x, y:U
H':Rplus U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rplus U R y0 z -> Rstar U R y0 z -> Rstar U R x0 z
-U:Type
R:Relation U
x, y:U
H':Rplus U R x y
forall x0 y0 : U, R x0 y0 -> Rstar U R x0 y0 generalize Rstar_contains_R; intro T; red in T; auto with sets.
-U:Type
R:Relation U
x, y:U
H':Rplus U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rplus U R y0 z -> Rstar U R y0 z -> Rstar U R x0 z intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
Qed.

Theorem Rstar_transitive :
 forall (U:Type) (R:Relation U), Transitive U (Rstar U R).forall (U : Type) (R : Relation U),
Transitive U (Rstar U R)
Proof.forall (U : Type) (R : Relation U),
Transitive U (Rstar U R)
intros U R; red.U:Type
R:Relation U
forall x y z : U,
Rstar U R x y -> Rstar U R y z -> Rstar U R x z
intros x y z H'; elim H'; auto with sets.U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
forall x0 y0 z0 : U,
R x0 y0 ->
Rstar U R y0 z0 ->
(Rstar U R z0 z -> Rstar U R y0 z) ->
Rstar U R z0 z -> Rstar U R x0 z
intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets.
Qed.

Theorem Rstar_cases :
 forall (U:Type) (R:Relation U) (x y:U),
   Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y).forall (U : Type) (R : Relation U) (x y : U),
Rstar U R x y ->
x = y \/ (exists u : U, R x u /\ Rstar U R u y)
Proof.forall (U : Type) (R : Relation U) (x y : U),
Rstar U R x y ->
x = y \/ (exists u : U, R x u /\ Rstar U R u y)
intros U R x y H'; elim H'; auto with sets.U:Type
R:Relation U
x, y:U
H':Rstar U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z ->
y0 = z \/ (exists u : U, R y0 u /\ Rstar U R u z) ->
x0 = z \/ (exists u : U, R x0 u /\ Rstar U R u z)
intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets.
Qed.

Theorem Rstar_equiv_Rstar1 :
 forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).forall (U : Type) (R : Relation U),
same_relation U (Rstar U R) (Rstar1 U R)
Proof.forall (U : Type) (R : Relation U),
same_relation U (Rstar U R) (Rstar1 U R)
generalize Rstar_contains_R; intro T; red in T.T:forall (U : Type) (R : Relation U) (x y : U),
R x y -> Rstar U R x y
forall (U : Type) (R : Relation U),
same_relation U (Rstar U R) (Rstar1 U R)
intros U R; unfold same_relation, contains.T:forall (U0 : Type) (R0 : Relation U0) (x y : U0),
R0 x y -> Rstar U0 R0 x y
U:Type
R:Relation U
(forall x y : U, Rstar1 U R x y -> Rstar U R x y) /\
(forall x y : U, Rstar U R x y -> Rstar1 U R x y)
split; intros x y H'; elim H'; auto with sets.T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
R0 x0 y0 -> Rstar U0 R0 x0 y0
U:Type
R:Relation U
x, y:U
H':Rstar1 U R x y
forall x0 y0 z : U,
Rstar1 U R x0 y0 ->
Rstar U R x0 y0 ->
Rstar1 U R y0 z -> Rstar U R y0 z -> Rstar U R x0 z
T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
R0 x0 y0 -> Rstar U0 R0 x0 y0
U:Type
R:Relation U
x, y:U
H':Rstar U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z -> Rstar1 U R y0 z -> Rstar1 U R x0 z
-T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
R0 x0 y0 -> Rstar U0 R0 x0 y0
U:Type
R:Relation U
x, y:U
H':Rstar1 U R x y
forall x0 y0 z : U,
Rstar1 U R x0 y0 ->
Rstar U R x0 y0 ->
Rstar1 U R y0 z -> Rstar U R y0 z -> Rstar U R x0 z generalize Rstar_transitive; intro T1; red in T1.T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
R0 x0 y0 -> Rstar U0 R0 x0 y0
U:Type
R:Relation U
x, y:U
H':Rstar1 U R x y
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z -> Rstar U0 R0 x0 z
forall x0 y0 z : U,
Rstar1 U R x0 y0 ->
Rstar U R x0 y0 ->
Rstar1 U R y0 z -> Rstar U R y0 z -> Rstar U R x0 z
  intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
-T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
R0 x0 y0 -> Rstar U0 R0 x0 y0
U:Type
R:Relation U
x, y:U
H':Rstar U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z -> Rstar1 U R y0 z -> Rstar1 U R x0 z intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets.
Qed.

Theorem Rsym_imp_Rstarsym :
 forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).forall (U : Type) (R : Relation U),
Symmetric U R -> Symmetric U (Rstar U R)
Proof.forall (U : Type) (R : Relation U),
Symmetric U R -> Symmetric U (Rstar U R)
intros U R H'; red.U:Type
R:Relation U
H':Symmetric U R
forall x y : U, Rstar U R x y -> Rstar U R y x
intros x y H'0; elim H'0; auto with sets.U:Type
R:Relation U
H':Symmetric U R
x, y:U
H'0:Rstar U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z -> Rstar U R z y0 -> Rstar U R z x0
intros x0 y0 z H'1 H'2 H'3.U:Type
R:Relation U
H':Symmetric U R
x, y:U
H'0:Rstar U R x y
x0, y0, z:U
H'1:R x0 y0
H'2:Rstar U R y0 z
H'3:Rstar U R z y0
Rstar U R z x0
generalize Rstar_transitive; intro T1; red in T1.U:Type
R:Relation U
H':Symmetric U R
x, y:U
H'0:Rstar U R x y
x0, y0, z:U
H'1:R x0 y0
H'2:Rstar U R y0 z
H'3:Rstar U R z y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y1 z0 : U0),
Rstar U0 R0 x1 y1 ->
Rstar U0 R0 y1 z0 -> Rstar U0 R0 x1 z0
Rstar U R z x0
apply T1 with y0; auto with sets.U:Type
R:Relation U
H':Symmetric U R
x, y:U
H'0:Rstar U R x y
x0, y0, z:U
H'1:R x0 y0
H'2:Rstar U R y0 z
H'3:Rstar U R z y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y1 z0 : U0),
Rstar U0 R0 x1 y1 ->
Rstar U0 R0 y1 z0 -> Rstar U0 R0 x1 z0
Rstar U R y0 x0
apply Rstar_n with x0; auto with sets.
Qed.

Theorem Sstar_contains_Rstar :
 forall (U:Type) (R S:Relation U),
   contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).forall (U : Type) (R S : Relation U),
contains U (Rstar U S) R ->
contains U (Rstar U S) (Rstar U R)
Proof.forall (U : Type) (R S : Relation U),
contains U (Rstar U S) R ->
contains U (Rstar U S) (Rstar U R)
unfold contains.forall (U : Type) (R S : Relation U),
(forall x y : U, R x y -> Rstar U S x y) ->
forall x y : U, Rstar U R x y -> Rstar U S x y
intros U R S H' x y H'0; elim H'0; auto with sets.U:Type
R, S:Relation U
H':forall x0 y0 : U, R x0 y0 -> Rstar U S x0 y0
x, y:U
H'0:Rstar U R x y
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z -> Rstar U S y0 z -> Rstar U S x0 z
generalize Rstar_transitive; intro T1; red in T1.U:Type
R, S:Relation U
H':forall x0 y0 : U, R x0 y0 -> Rstar U S x0 y0
x, y:U
H'0:Rstar U R x y
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z -> Rstar U0 R0 x0 z
forall x0 y0 z : U,
R x0 y0 ->
Rstar U R y0 z -> Rstar U S y0 z -> Rstar U S x0 z
intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets.
Qed.

Theorem star_monotone :
 forall (U:Type) (R S:Relation U),
   contains U S R -> contains U (Rstar U S) (Rstar U R).forall (U : Type) (R S : Relation U),
contains U S R -> contains U (Rstar U S) (Rstar U R)
Proof.forall (U : Type) (R S : Relation U),
contains U S R -> contains U (Rstar U S) (Rstar U R)
intros U R S H'.U:Type
R, S:Relation U
H':contains U S R
contains U (Rstar U S) (Rstar U R)
apply Sstar_contains_Rstar; auto with sets.U:Type
R, S:Relation U
H':contains U S R
contains U (Rstar U S) R
generalize (Rstar_contains_R U S); auto with sets.
Qed.

Theorem RstarRplus_RRstar :
 forall (U:Type) (R:Relation U) (x y z:U),
   Rstar U R x y -> Rplus U R y z ->  exists u : _, R x u /\ Rstar U R u z.forall (U : Type) (R : Relation U) (x y z : U),
Rstar U R x y ->
Rplus U R y z -> exists u : U, R x u /\ Rstar U R u z
Proof.forall (U : Type) (R : Relation U) (x y z : U),
Rstar U R x y ->
Rplus U R y z -> exists u : U, R x u /\ Rstar U R u z
generalize Rstar_contains_Rplus; intro T; red in T.T:forall (U : Type) (R : Relation U) (x y : U),
Rplus U R x y -> Rstar U R x y
forall (U : Type) (R : Relation U) (x y z : U),
Rstar U R x y ->
Rplus U R y z -> exists u : U, R x u /\ Rstar U R u z
generalize Rstar_transitive; intro T1; red in T1.T:forall (U : Type) (R : Relation U) (x y : U),
Rplus U R x y -> Rstar U R x y
T1:forall (U : Type) (R : Relation U) (x y z : U),
Rstar U R x y -> Rstar U R y z -> Rstar U R x z
forall (U : Type) (R : Relation U) (x y z : U),
Rstar U R x y ->
Rplus U R y z -> exists u : U, R x u /\ Rstar U R u z
intros U R x y z H'; elim H'.T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
Rplus U0 R0 x0 y0 -> Rstar U0 R0 x0 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z0 : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x0 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
forall x0 : U,
Rplus U R x0 z ->
exists u : U, R x0 u /\ Rstar U R u z
T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
Rplus U0 R0 x0 y0 -> Rstar U0 R0 x0 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z0 : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x0 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
forall x0 y0 z0 : U,
R x0 y0 ->
Rstar U R y0 z0 ->
(Rplus U R z0 z ->
 exists u : U, R y0 u /\ Rstar U R u z) ->
Rplus U R z0 z ->
exists u : U, R x0 u /\ Rstar U R u z
-T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
Rplus U0 R0 x0 y0 -> Rstar U0 R0 x0 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z0 : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x0 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
forall x0 : U,
Rplus U R x0 z ->
exists u : U, R x0 u /\ Rstar U R u z intros x0 H'0; elim H'0.T:forall (U0 : Type) (R0 : Relation U0) (x1 y0 : U0),
Rplus U0 R0 x1 y0 -> Rstar U0 R0 x1 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0:U
H'0:Rplus U R x0 z
forall x1 y0 : U,
R x1 y0 -> exists u : U, R x1 u /\ Rstar U R u y0
T:forall (U0 : Type) (R0 : Relation U0) (x1 y0 : U0),
Rplus U0 R0 x1 y0 -> Rstar U0 R0 x1 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0:U
H'0:Rplus U R x0 z
forall x1 y0 z0 : U,
R x1 y0 ->
Rplus U R y0 z0 ->
(exists u : U, R y0 u /\ Rstar U R u z0) ->
exists u : U, R x1 u /\ Rstar U R u z0
  +T:forall (U0 : Type) (R0 : Relation U0) (x1 y0 : U0),
Rplus U0 R0 x1 y0 -> Rstar U0 R0 x1 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0:U
H'0:Rplus U R x0 z
forall x1 y0 : U,
R x1 y0 -> exists u : U, R x1 u /\ Rstar U R u y0 intros x1 y0 H'1; exists y0; auto with sets.
  +T:forall (U0 : Type) (R0 : Relation U0) (x1 y0 : U0),
Rplus U0 R0 x1 y0 -> Rstar U0 R0 x1 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0:U
H'0:Rplus U R x0 z
forall x1 y0 z0 : U,
R x1 y0 ->
Rplus U R y0 z0 ->
(exists u : U, R y0 u /\ Rstar U R u z0) ->
exists u : U, R x1 u /\ Rstar U R u z0 intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets.
-T:forall (U0 : Type) (R0 : Relation U0) (x0 y0 : U0),
Rplus U0 R0 x0 y0 -> Rstar U0 R0 x0 y0
T1:forall (U0 : Type) (R0 : Relation U0)
  (x0 y0 z0 : U0),
Rstar U0 R0 x0 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x0 z0
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
forall x0 y0 z0 : U,
R x0 y0 ->
Rstar U R y0 z0 ->
(Rplus U R z0 z ->
 exists u : U, R y0 u /\ Rstar U R u z) ->
Rplus U R z0 z ->
exists u : U, R x0 u /\ Rstar U R u z intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0.T:forall (U0 : Type) (R0 : Relation U0) (x1 y1 : U0),
Rplus U0 R0 x1 y1 -> Rstar U0 R0 x1 y1
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y1 z1 : U0),
Rstar U0 R0 x1 y1 ->
Rstar U0 R0 y1 z1 -> Rstar U0 R0 x1 z1
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0, y0, z0:U
H'0:R x0 y0
H'1:Rstar U R y0 z0
H'2:Rplus U R z0 z -> exists u : U, R y0 u /\ Rstar U R u z
H'3:Rplus U R z0 z
R x0 y0 /\ Rstar U R y0 z
  split; [ try assumption | idtac ].T:forall (U0 : Type) (R0 : Relation U0) (x1 y1 : U0),
Rplus U0 R0 x1 y1 -> Rstar U0 R0 x1 y1
T1:forall (U0 : Type) (R0 : Relation U0)
  (x1 y1 z1 : U0),
Rstar U0 R0 x1 y1 ->
Rstar U0 R0 y1 z1 -> Rstar U0 R0 x1 z1
U:Type
R:Relation U
x, y, z:U
H':Rstar U R x y
x0, y0, z0:U
H'0:R x0 y0
H'1:Rstar U R y0 z0
H'2:Rplus U R z0 z -> exists u : U, R y0 u /\ Rstar U R u z
H'3:Rplus U R z0 z
Rstar U R y0 z
  apply T1 with z0; auto with sets.
Qed.

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.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 : U, Rstar U R a z /\ R b z
Proof.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 : U, Rstar U R a z /\ R b z
intros U R H' x b H'0; elim H'0.U:Type
R:Relation U
H':Strongly_confluent U R
x, b:U
H'0:Rstar U R x b
forall x0 a : U,
R x0 a -> exists z : U, Rstar U R a z /\ R x0 z
U:Type
R:Relation U
H':Strongly_confluent U R
x, b:U
H'0:Rstar U R x b
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall a : U,
 R y a -> exists z0 : U, Rstar U R a z0 /\ R z z0) ->
forall a : U,
R x0 a -> exists z0 : U, Rstar U R a z0 /\ R z z0
-U:Type
R:Relation U
H':Strongly_confluent U R
x, b:U
H'0:Rstar U R x b
forall x0 a : U,
R x0 a -> exists z : U, Rstar U R a z /\ R x0 z intros x0 a H'1; exists a; auto with sets.
-U:Type
R:Relation U
H':Strongly_confluent U R
x, b:U
H'0:Rstar U R x b
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall a : U,
 R y a -> exists z0 : U, Rstar U R a z0 /\ R z z0) ->
forall a : U,
R x0 a -> exists z0 : U, Rstar U R a z0 /\ R z z0 intros x0 y z H'1 H'2 H'3 a H'4.U:Type
R:Relation U
H':Strongly_confluent U R
x, b:U
H'0:Rstar U R x b
x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
a:U
H'4:R x0 a
exists z0 : U, Rstar U R a z0 /\ R z z0
  red in H'.U:Type
R:Relation U
H':forall x1 a0 b0 : U,
R x1 a0 ->
R x1 b0 -> exists z0 : U, R a0 z0 /\ R b0 z0
x, b:U
H'0:Rstar U R x b
x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
a:U
H'4:R x0 a
exists z0 : U, Rstar U R a z0 /\ R z z0
  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.U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
exists z0 : U, Rstar U R a z0 /\ R z z0
  elim H'9.U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
forall x1 : U,
R a x1 /\ R y x1 ->
exists z0 : U, Rstar U R a z0 /\ R z z0
  intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
t:U
H'6:R a t
H'7:R y t
exists z0 : U, Rstar U R a z0 /\ R z z0
  elim (H'3 t); auto with sets.U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
t:U
H'6:R a t
H'7:R y t
forall x1 : U,
Rstar U R t x1 /\ R z x1 ->
exists z0 : U, Rstar U R a z0 /\ R z z0
  intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U, R y a0 -> exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
t:U
H'6:R a t
H'7:R y t
z1:U
H'8:Rstar U R t z1
H'10:R z z1
exists z0 : U, Rstar U R a z0 /\ R z z0
  exists z1; split; [ idtac | assumption ].U:Type
R:Relation U
x0, y, a, x, b:U
H'0:Rstar U R x b
z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall a0 : U,
R y a0 ->
exists z0 : U, Rstar U R a0 z0 /\ R z z0
H'4:R x0 a
H'9:exists z0 : U, R a z0 /\ R y z0
t:U
H'6:R a t
H'7:R y t
z1:U
H'8:Rstar U R t z1
H'10:R z z1
Rstar U R a z1
  apply Rstar_n with t; auto with sets.
Qed.