fact: Parameter add_eq_o : forall m x y e, E.eq x y -> find y (add x e m) = Some e.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)