proposition: Lemma sym_eq_forall_eq : forall R, sym R = (forall x y, R x y = R y x).
proof: Proof. Proof using. unfold sym. extens. iff M. { extens*. } { intros. rewrite* M. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)