proposition: Lemma updateE r k (f : update k r) : untag f = k :+ r.
proof: Proof. by case: f=>[[j]] /=; rewrite /update_axiom /= => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)