proposition: Lemma empty_in_iff x : In x (@empty elt) <-> False.
proof: Proof. split; [ apply not_in_empty | destruct 1 ]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)