proposition: Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) : x ≡ y ↔ x = y.
proof: Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)