proposition: Lemma lookup_remove_eq: forall k s, lookup k (remove k s) = None.
proof: Proof. intros. match goal with |- ?x = _ => destruct x eqn:EQ end; [| reflexivity]. rewrite mapsto_lookup in EQ. exfalso; eapply mapsto_remove_eq; eauto. Qed.
imports: Coq(Morphisms) ExtLib(Core.RelDec) Paco(paco) ITree(Basics.HeterogeneousRelations ITree ITreeFacts Eq.Paco2 Events.State Events.StateFacts Events.MapDefault)