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