proposition: Lemma in_add_2: forall T x y (z: T) d, In x d -> In x (add y z d).
proof: Proof. intros. destruct (E.eq_dec y x). exists z. auto with map. destruct H as [w ?]. exists w. auto with map. Qed.
imports: Coq(FMaps) ATBR(Common) ATBR(BoolView)