proposition: Lemma xelements_spec: forall s j acc y, InL y (xelements s j acc) <-> InL y acc \/ exists x, y=(j@x) /\ mem x s = true.
proof: Proof. induction s as [|l IHl o r IHr]; simpl. - intros. split; intro H. + left. assumption. + destruct H as [H|[x [Hx Hx']]]. * assumption. * discriminate. - intros j acc y. case o. + rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split. * intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto. -- right. exists x~1. auto. -- right. exists x~0. auto. * intros [H|[x [-> H]]]. -- eauto. -- destruct x. ++ left. right. right. exists x; auto. ++ right. exists x; auto. ++ left. left. reflexivity. + rewrite IHl, IHr. clear IHl IHr. split. * intros [[H|[x [-> H]]]|[x [-> H]]]. -- eauto. -- right. exists x~1. auto. -- right. exists x~0. auto. * intros [H|[x [-> H]]]. -- eauto. -- destruct x. ++ left. right. exists x; auto. ++ right. exists x; auto. ++ discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface