proposition: Lemma height_0 : forall l, avl l -> height l = 0 -> l = Leaf _.
proof: Proof. destruct 1; intuition; simpl in *. avl_nns; simpl in *; exfalso; omega_max. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia