proposition: Lemma add_valid: forall acc f i p B, valid f i p /\ approx f acc /\ B -> StateMap.MapsTo i p (StateMap.add i p acc) /\ approx f (StateMap.add i p acc) /\ B.
proof: Proof. intros. unfold approx. StateMapProps.map_iff. intuition. revert H1. StateMapProps.map_iff. intuition; subst; trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(Utils_WF) Coq(Relations) Coq(Eqdep_dec)