proposition: Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. intros m x y e; exact (@remove_2 elt _ x y e (is_bst m)). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia