proposition: Lemma foundy_pf x y (s : Search.form x) : axiom x y (foundy_tag (y :: s)).
proof: Proof. move: s=>[[s]]; rewrite /Search.axiom /= /axiom !inE eq_refl /= => H1. by rewrite H1 orbT; split=>//; case/andP=>H2 _; case: eqP H1 H2=>// -> ->. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)