proposition: Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 -> avl (map2_opt m1 m2).
proof: Proof. intros m1 m2; functional induction (map2_opt m1 m2); auto; factornode _x0 _x1 _x2 _x3 _x4 as r2; intros; destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl; auto using join_avl, concat_avl. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia