proposition: Lemma add_eq_o : forall A m x y e, E.eq x y -> @find A y (add x e m) = Some e.
proof: Proof. intros. unfold find. apply F.add_eq_o. rewrite H. reflexivity. Qed.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)