proposition: Lemma map2_opt_bst : forall m m', bst m -> bst m' -> bst (map2_opt m m').
proof: Proof. intros m m'; functional induction (map2_opt m m'); intros; auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); rewrite e1; simpl in *; destruct 3. - apply join_bst; auto. + intros y Hy; specialize H with y. destruct (map2_opt_2 H1 H6 Hy); intuition. + intros y Hy; specialize H5 with y. destruct (map2_opt_2 H2 H7 Hy); intuition. - apply concat_bst; auto. intros y y' Hy Hy'; specialize H with y; specialize H5 with y'. apply X.lt_trans with x1. + destruct (map2_opt_2 H1 H6 Hy); intuition. + destruct (map2_opt_2 H2 H7 Hy'); intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int