proposition: Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y.
proof: Proof. split. - intros [? HYX]. split; [ done | by intros <- ]. - intros [? HXY]. split; [ done | by contradict HXY; apply (anti_symm R) ]. Qed.
imports: stdpp(options)