~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- let pbo = CicMetaSubst.apply_subst subst pbo in
+ let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
let pty = CicMetaSubst.apply_subst subst pty in
let term =
match term with