proposition: Lemma subset_spec: forall s s', subset s s' = true <-> s [<=] s'.
proof: Proof. induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl. - split; intros. + apply subset_Leaf_s. + reflexivity. - split; intros. + apply subset_Leaf_s. + reflexivity. - rewrite <- 2andb_lazy_alt, 2andb_true_iff, 2is_empty_spec. destruct o; simpl. + split. * intuition discriminate. * intro H. elim (@empty_spec 1). apply H. reflexivity. + split; intro H. * destruct H as [[_ Hl] Hr]. intros [i|i|] Hi. -- elim (Hr i Hi). -- elim (Hl i Hi). -- discriminate. * split. -- split. ++ reflexivity. ++ unfold Empty. intros a H1. apply (@empty_spec (a~0)), H. assumption. -- unfold Empty. intros a H1. apply (@empty_spec (a~1)), H. assumption. - rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear. destruct o; simpl. + split; intro H. * destruct H as [[Ho' Hl] Hr]. rewrite Ho'. intros i Hi. destruct i. -- apply (Hr i). assumption. -- apply (Hl i). assumption. -- assumption. * split. -- split. ++ destruct o'; trivial. specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity. ++ intros i Hi. apply (H i~0). apply Hi. -- intros i Hi. apply (H i~1). apply Hi. + split; intros. * intros i Hi. destruct i; destruct H as [[H Hl] Hr]. -- apply (Hr i). assumption. -- apply (Hl i). assumption. -- discriminate Hi. * split. -- split. ++ reflexivity. ++ intros i Hi. apply (H i~0). apply Hi. -- intros i Hi. apply (H i~1). apply Hi. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface