proposition: Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> In y (map2_opt m m') -> In y m \/ In y m'.
proof: Proof. intros m m'; functional induction (map2_opt m m'); intros; auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; try (generalize (split_in_1 x1 H0 y)(split_in_2 x1 H0 y) (split_bst x1 H0); rewrite e1; simpl; destruct 3; inv bst). - right; apply find_in. generalize (in_find (mapr_bst H0) H1); rewrite mapr_f0; auto. destruct (find y m2); auto; intros; discriminate. - factornode l1 x1 d1 r1 _x as m1. left; apply find_in. generalize (in_find (mapl_bst H) H1); rewrite mapl_f0; auto. destruct (find y m1); auto; intros; discriminate. - rewrite join_in in H1; destruct H1 as [H'|[H'|H']]; auto. + destruct (IHt1 y H6 H4 H'); intuition. + destruct (IHt0 y H7 H5 H'); intuition. - rewrite concat_in in H1; destruct H1 as [H'|H']; auto. + destruct (IHt1 y H6 H4 H'); intuition. + destruct (IHt0 y H7 H5 H'); intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int