~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let with_what, metasenv, u = with_what context metasenv u in
let with_what = CicMetaSubst.apply_subst subst with_what in
let pbo = CicMetaSubst.apply_subst subst pbo in
let pty = CicMetaSubst.apply_subst subst pty in
~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let with_what, metasenv, u = with_what context metasenv u in
let with_what = CicMetaSubst.apply_subst subst with_what in
let pbo = CicMetaSubst.apply_subst subst pbo in
let pty = CicMetaSubst.apply_subst subst pty in