proposition: Lemma unguard_union_pf A ts1 ts2 (u1 : @unguarded_form A ts1) (u2 : @unguarded_form A ts2) : unguard_ax (UnOmf ts1 ts2) (union_tag (untag u1 \+ untag u2)).
proof: Proof. by case: u1 u2=>u1 pf1 [u2 pf2]; rewrite /= pf1 pf2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)