proposition: Lemma isundef_sound i ts : all (wf i) ts -> isundef i ts -> ~~ valid (interp i ts).
proof: Proof. elim: ts=>[|t ts IH] //= /andP [W A]. case: t W=>[n v|n] /= /size_onth [k] X; rewrite /isundef /= X; last first. - rewrite orbCA=>H; case: validUn=>// V; rewrite (negbTE (IH A _)) //. by case/orP: H V=>// /undefbE ->; rewrite valid_undef. rewrite negb_and negbK has_getkeys -orbA /=. case/orP=>// V; last by rewrite validPtUn andbCA (negbTE (IH A _)). by case: (keyP V X)=>u ->; rewrite joinA pts_undef2 undef_join valid_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)