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