selected_terms_with_context ([],[]) in
let t1 = CicMetaSubst.apply_subst subst t1 in
let t2 = CicMetaSubst.apply_subst subst t2 in
+ let ty = CicMetaSubst.apply_subst subst ty in
let equality = CicMetaSubst.apply_subst subst equality in
let abstr_gty =
ProofEngineReduction.replace_lifting_csc 0