proposition: Lemma mapi_avl : forall m, avl m -> avl (mapi f m).
proof: Proof. induction m; simpl; auto. inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia