let pty = CicMetaSubst.apply_subst subst pty in
let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =
let pty = CicMetaSubst.apply_subst subst pty in
let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =