proposition: Lemma map_option_avl : forall m, avl m -> avl (map_option f m).
proof: Proof. induction m; simpl; auto; intros. inv avl; destruct (f k e); auto using join_avl, concat_avl. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia