proposition: Lemma left_pfU h k r (f : uform k r) : uform_axiom k (r \+ h) (left_tagU (untagU f \+ h)).
proof: Proof. case: f=>f; rewrite /uform_axiom /= =>->. by rewrite joinA. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)