proposition: Lemma is_empty_spec: forall s, is_empty s = true <-> Empty s.
proof: Proof. unfold Empty, In. induction s as [|l IHl o r IHr]; simpl. - firstorder. - rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr. destruct o; simpl; split. + intuition discriminate. + intro H. elim (H 1). reflexivity. + intros H [a|a|]; apply H || intro; discriminate. + intro H. split. * split. -- reflexivity. -- intro a. apply (H a~0). * intro a. apply (H a~1). Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface