proposition: Lemma union_pf s1 s2 (h1 : form s1) (h2 : form s2) : axiom (union_tag (h1 :+ h2)) (s1 ++ s2).
proof: Proof. move:h1 h2=>[[i1]] H1 [[i2]] H2; rewrite /axiom /= in H1 H2 * => D. case/(_ (defUnl D)): H1=>U1 H1; case/(_ (defUnr D)): H2=>U2 H2. split=>[|x]; last first. - rewrite mem_cat; case/orP; [move/H1 | move/H2]; by rewrite domUn !inE /= D => -> //=; rewrite orbT. rewrite cat_uniq U1 U2 andbT -all_predC. apply/allP=>x; move/H2=>H3; apply: (introN idP); move/H1=>H4. by case: defUn D=>// _ _; move/(_ _ H4); rewrite H3. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)