proposition: Lemma interp_subctx j k t: valid j t -> subctx j k -> interp j t = interp k t.
proof: Proof. move=>I [S1 S2]; elim:t I=>[//|e t IH]. rewrite 2!interp_cons valid_cons; case/andP=>H1. move/IH=>->; case: e H1=>[x d|v] /=; rewrite /valid /= !andbT; move/prefix_onth; by [move/(_ _ S2)=>-> | move/(_ _ S1)=>->]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)