proposition: Lemma union_pf i j k ts1 ts2 (f1 : form i j ts1) (f2 : form j k ts2) : axiom i k (ts1 ++ ts2) (union_tag (untag f1 \+ untag f2)).
proof: Proof. case: f1 f2=>_ [<- S1 W1][_][<- S2 W2]; split. - by rewrite /interp foldr_cat fE joinC -(sc_interp S2 W1). - by apply: sc_trans S1 S2. by rewrite all_cat (sc_wf S2 W1) W2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)