proposition: Lemma union_pf i j k t1 t2 (f1 : ast i j t1) (f2 : ast j k t2) : invariant i k (t1 ++ t2) (union_tag (f1 :+ f2)).
proof: Proof. case: f1 f2=>h1 /= [<- S1 D1] [h2 /= [<- S2 D2]]. split; first by rewrite interp_cat (interp_subctx D1 S2). - by apply: (subctx_trans S1 S2). by rewrite valid_cat D2 andbT; apply: (valid_subctx S2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)