proposition: Lemma rtclosure_ind_r : forall R (P : A -> A -> Prop), (forall x, P x x) -> (forall y x z, rtclosure R x y -> P x y -> R y z -> P x z) -> (forall x y, rtclosure R x y -> P x y).
proof: Proof. Proof using. introv H1 H2 M. rewrite rtclosure_eq_rtclosure'r in *. induction* M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)