proposition: Lemma valid_cat j t1 t2 : valid j (t1 ++ t2) = valid j t1 && valid j t2.
proof: Proof. rewrite /valid valid_ptrs_cat valid_heaps_cat. by rewrite -!andbA -!(andbCA (valid_ptrs j t2)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)