proposition: Lemma valid_heaps_cat j t1 t2 : valid_heaps j (t1 ++ t2) = valid_heaps j t1 && valid_heaps j t2.
proof: Proof. elim: t1 t2=>[//|v t1 IH /=] t2. by case: v=>[x d | v]; rewrite IH // andbA. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)