proposition: Lemma sc_interp i j ts : sub_ctx i j -> all (wf i) ts -> interp i ts = interp j ts.
proof: Proof. move=>H; elim: ts=>[|t ts IH] //= /andP [H0] /IH ->. by case: t H0=>n /= /prefix_onth <-. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)