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