proposition: Lemma lookup_remove_neq: forall k k' s, k <> k' -> lookup k (remove k' s) = lookup k s.
proof: Proof. intros. match goal with |- ?x = _ => destruct x eqn:EQ end. - rewrite mapsto_lookup in EQ. apply mapsto_remove_neq in EQ; auto. symmetry; rewrite mapsto_lookup; eauto. - match goal with |- _ = ?x => destruct x eqn:EQ' end; auto. rewrite mapsto_lookup in EQ'. eapply mapsto_remove_neq in EQ'; eauto. rewrite <- mapsto_lookup in EQ'. rewrite EQ in EQ'; inv EQ'. Unshelve. all: typeclasses eauto. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)