proposition: Lemma equal_or_subset_and_not_equal_subset {x y} : (Equal x y \/ (Subset x y /\ ~Equal x y)) <-> Subset x y.
proof: Proof. destruct (equal x y) eqn:?; simpl; bool_congr; to_caps; simplify_sets; intuition. Qed.
imports: Coq.MSets.MSetInterface Coq.MSets.MSetProperties Coq.MSets.MSetFacts Coq.MSets.MSetDecide Fiat.Common.Instances Fiat.Common.BoolFacts Fiat.Common