proposition: Lemma rsclosure_eq : forall R x y, rsclosure R x y = (R x y \/ R y x \/ x = y).
proof: Proof. Proof using. extens. iff M. { induction* M. } { destruct M as [M|[M|M]]; subst*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)