proposition: Lemma bal_in : forall l x e r y, In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r.
proof: Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; rewrite !create_in; intuition_in. Qed.
imports: FunInd FMapInterface FMapList ZArith Int