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