proposition: Lemma valid_subctx i j t : subctx i j -> valid i t -> valid j t.
proof: Proof. case: i j=>hs1 xs1 [hs2 xs2][/= P1 P2]. elim: t=>[//|e t IH]; rewrite -cat1s 2!valid_cat. case/andP=>H; move/IH=>->. case: e H=>[x d| v]; rewrite /valid /= !andbT => H; apply: leq_trans H _; by [apply: (prefix_size P2) | apply: (prefix_size P1)]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)