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