proposition: Lemma left_pf h r (f : forall k, form k r) k : form_axiom k (r \+ h) (left_tag (untag (f k) \+ h)).
proof: Proof. by rewrite formE /form_axiom /= joinA. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)