fact: Definition wf i t := match t with Pts n _ => n < size (keyx i) | Var n => n < size (varx i) end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)