proposition: Lemma subsetl_spec : forall subset_l1 l1 x1 c1 s2 `{Ok (Node c1 l1 x1 Leaf), Ok s2}, (forall s `{Ok s}, (subset_l1 s = true <-> Subset l1 s)) -> (subsetl subset_l1 x1 s2 = true <-> Subset (Node c1 l1 x1 Leaf) s2 ).
proof: Proof. induction s2 as [|c2 l2 IHl2 x2 r2 IHr2]; simpl; intros. - unfold Subset; intuition; try discriminate. assert (H': InT x1 Leaf) by auto; inversion H'. - specialize (IHl2 H). specialize (IHr2 H). inv. elim_compare x1 x2. + rewrite H1 by auto; clear H1 IHl2 IHr2. 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. + rewrite IHl2 by auto; clear H1 IHl2 IHr2. 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, H1 by auto; clear H1 IHl2 IHr2. unfold Subset. intuition_in. * constructor 3. setoid_replace a with x1; auto. rewrite <- mem_spec; auto. * rewrite mem_spec; auto. assert (InT x1 (Node c2 l2 x2 r2)) by auto; intuition_in; order. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat