~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in