fact: Definition undefx i t := if t is Var n then if onth (varx i) n is Some x then undefb x else false else false.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)