proposition: Lemma append_avl s1 s2 `{!Avl s1, !Avl s2} : -(2) <= height s1 - height s2 <= 2 -> Avl (append s1 s2).
proof: Proof. intros; now destruct (@append_avl_1 s1 s2). Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)