proposition: Lemma lookup_add_neq: forall k k' v s, k' <> k -> lookup k (add k' v s) = lookup k s.
proof: Proof. intros. generalize (@mapsto_add_neq _ _ _ eq _ _ s k' v k H); clear H; intros H. setoid_rewrite <- mapsto_lookup in H. destruct (lookup k s) as [v' |] eqn:EQ. - specialize (H v'). apply H; auto. - destruct (lookup k (add k' v s)) as [v' |] eqn:EQ'; [| reflexivity]. specialize (H v'). symmetry; apply H; auto. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)