proposition: Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s.
proof: Proof. induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial. - destruct o. + reflexivity. + rewrite andb_comm. reflexivity. - rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true. rewrite 7andb_true_iff, eqb_true_iff. rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst. + destruct o'; reflexivity. + destruct o'; reflexivity. + destruct o; auto. destruct o'; trivial. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface