proposition: Lemma sc_wf i j ts : sub_ctx i j -> all (wf i) ts -> all (wf j) ts.
proof: Proof. move/prefix_size=>H; elim: ts=>[|t ts IH] //=. case/andP=>Hi /IH ->; rewrite andbT. by case: t Hi=>v /= Hi; apply: leq_trans H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)