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