proposition: Lemma find_spec : forall A k s, find_spec_ind A k s (find k s).
proof: Proof. intros. case_eq (find k s); intros; constructor; auto with map. intros [x Hx]. apply find_1 in Hx. rewrite H in Hx. discriminate. Qed.
imports: Coq(FMaps) ATBR(Common) ATBR(BoolView)