fact: Definition interp' i t := match t with Pts n v => if onth (keyx i) n is Some k then pts k v else undef | Var n => if onth (varx i) n is Some f then f else undef end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)