proposition: Lemma foundz_pf x y z (s : form x y) : axiom x y (foundz_tag (z :: s)).
proof: Proof. move: s=>[[s]]; case=>/= H1 H2 H3. rewrite /axiom /= !inE /= H1 H2 !orbT; split=>//. by case/andP=>_; apply: H3. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)