proposition: Lemma valid_wf i ts : valid (interp i ts) -> all (wf i) ts.
proof: Proof. elim: ts=>[|t ts IH] //= V; rewrite (IH (validR V)) andbT. case: t {V IH} (validL V)=>[n v|n] /=; by case X : (onth _ _)=>[a|]; rewrite ?(onth_size X) // valid_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)