proposition: Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'.
proof: Proof. unfold In, map2; intros elt elt' elt'' m m' x f. do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. - apply (is_bst m). - apply (is_bst m'). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia