proposition: Lemma not_rsclosure_inv : forall R x y, ~ rsclosure R x y -> ~ R x y /\ ~ R y x /\ ~ x = y.
proof: Proof. Proof using. introv M. rewrite* rsclosure_eq in M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)