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