fact: Definition EnsembleUpdateKey (k : Key) (ens : Ensemble (Key * Value)) (f : Value -> Value) (kv : Key * Value) : Prop := ((fst kv) = k /\ exists v, (snd kv) = f v /\ In _ ens (k, v)) \/ (EnsembleRemoveKey k ens kv).
imports: Coq.Sets.Ensembles