proposition: Lemma lookup_add_eq: forall k v s, lookup k (add k v s) = Some v.
proof: Proof. intros. rewrite mapsto_lookup; apply mapsto_add_eq. Unshelve. 2: typeclasses eauto. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)