proposition: Lemma bal_mapsto : forall l x e r y e', MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r).
proof: Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; unfold assert_false, create; intuition_in. Qed.
imports: FunInd FMapInterface FMapList ZArith Int