+ let b = NCicReduction.alpha_eq metasenv subst context p t in
+ if not b then None else
+ let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+ let pis =
+ let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
+ aux ty
+ in
+ Some (p,pis - arity - cpos - 1,cpos)