proposition: Lemma right_pf h r (f : forall k, update k r) k : update_axiom k (h :+ r) (right_tag (h :+ f k)).
proof: Proof. by rewrite updateE /update_axiom /= unCA. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)