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