proposition: Lemma empty_o : forall A x, find x (empty A) = None.
proof: Proof. intros. unfold find. apply F.empty_o. Qed.
imports: Coq(ZArith) Coq(FMapInterface FMapPositive) Coq(FMapList FMapFacts) Coq(String Ascii List) StructTact(StructTactics StringOrders)