proposition: Lemma head_pfU k : uform_axiom k Unit (head_tagU k).
proof: Proof. by rewrite /uform_axiom unitR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)