proposition: Lemma irrefl_eq_forall_neq : forall R, irrefl R = (forall x y, R x y -> x <> y).
proof: Proof. Proof using. unfold irrefl. extens. iff M. { introv H E. subst*. } { autos*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)