proposition: Theorem Rstar_reflexive : forall x : A, Rstar x x.
proof: Proof. Proof fun (x : A) (P : A -> A -> Prop) (h1 : forall u : A, P u u) (h2 : forall u v w : A, R u v -> P v w -> P u w) => h1 x. Theorem Rstar_R : forall x y z : A, R x y -> Rstar y z -> Rstar x z. Proof fun (x y z : A) (t1 : R x y) (t2 : Rstar y z) (P : A -> A -> Prop) (h1 : forall u : A, P u u) (h2 : forall u v w : A, R u v -> P v w -> P u w) => h2 x y z t1 (t2 P h1 h2). Theorem Rstar_transitive : forall x y z : A, Rstar x y -> Rstar y z -> Rstar x z. Proof fun (x y z : A) (h : Rstar x y) => h (fun u v : A => Rstar v z -> Rstar u z) (fun (u : A) (t : Rstar u z) => t) (fun (u v w : A) (t1 : R u v) (t2 : Rstar w z -> Rstar v z) (t3 : Rstar w z) => Rstar_R u v z t1 (t2 t3)). Definition Rstar' (x y : A) := forall P : A -> A -> Prop, P x x -> (forall u : A, R x u -> Rstar u y -> P x y) -> P x y. Theorem Rstar'_reflexive : forall x : A, Rstar' x x. Proof fun (x : A) (P : A -> A -> Prop) (h : P x x) (h' : forall u : A, R x u -> Rstar u x -> P x x) => h. Theorem Rstar'_R : forall x y z : A, R x z -> Rstar z y -> Rstar' x y. Proof fun (x y z : A) (t1 : R x z) (t2 : Rstar z y) (P : A -> A -> Prop) (h1 : P x x) (h2 : forall u : A, R x u -> Rstar u y -> P x y) => h2 z t1 t2. Theorem Rstar'_Rstar : forall x y : A, Rstar' x y -> Rstar x y. Proof fun (x y : A) (h : Rstar' x y) => h Rstar (Rstar_reflexive x) (fun u : A => Rstar_R x u y). Theorem Rstar_Rstar' : forall x y : A, Rstar x y -> Rstar' x y. Proof fun (x y : A) (h : Rstar x y) => h Rstar' (fun u : A => Rstar'_reflexive u) (fun (u v w : A) (h1 : R u v) (h2 : Rstar' v w) => Rstar'_R u w v h1 (Rstar'_Rstar v w h2)). Lemma Rstar_inv : forall x y : A, Rstar x y -> x = y \/ ex2 (fun z : A => R x z) (fun z : A => Rstar z y). intros x y Rstar_x_y. pattern x, y in |- *. apply Rstar_x_y. auto. intros u v w R_u_v Hyp. apply or_intror. exists v. assumption. elim Hyp. intro Rew. rewrite Rew. apply Rstar_reflexive. intro temp; elim temp; clear temp. intros z R_v_z Rstar_z_w. apply Rstar_R with z; assumption. Qed.