proposition: Lemma sclosure_eq_of_sym : forall R, sym R -> sclosure R = R.
proof: Proof. Proof using. unfolds sym. introv H. extens. intros. rewrite sclosure_eq. iff M. { destruct M; subst*. } { auto. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)