proposition: Lemma subset_spec : forall s1 s2 `{Ok s1, Ok s2}, (subset s1 s2 = true <-> Subset s1 s2).
proof: Proof. induction s1 as [|c1 l1 IHl1 x1 r1 IHr1]; simpl; intros. - unfold Subset; intuition_in. - destruct s2 as [|c2 l2 x2 r2]; simpl; intros. + unfold Subset; intuition_in; try discriminate. assert (H': InT x1 Leaf) by auto; inversion H'. + inv. elim_compare x1 x2. * rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto. clear IHl1 IHr1. unfold Subset; intuition_in. -- assert (X.eq a x2) by order; intuition_in. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. * rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto. rewrite (@subsetl_spec (subset l1) l1 x1 c1) by auto. clear IHl1 IHr1. unfold Subset; intuition_in. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. * rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto. rewrite (@subsetr_spec (subset r1) r1 x1 c1) by auto. clear IHl1 IHr1. unfold Subset; intuition_in. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. -- assert (InT a (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat