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