proposition: Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 -> -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2).
proof: Proof. intros; generalize (merge_avl_1 H H0 H1); intuition. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia