proposition: Lemma subsetr_spec : forall subset_r1 r1 x1 c1 s2, bst (Node c1 Leaf x1 r1) -> bst s2 -> (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) -> (subsetr subset_r1 x1 s2 = true <-> Subset (Node c1 Leaf x1 r1) 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 <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2. unfold Subset. intuition_in. * constructor 2. 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. + rewrite IHr2 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. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat