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