selected_terms_with_context ([],[]) in
let t1 = CicMetaSubst.apply_subst subst t1 in
let t2 = CicMetaSubst.apply_subst subst t2 in
selected_terms_with_context ([],[]) in
let t1 = CicMetaSubst.apply_subst subst t1 in
let t2 = CicMetaSubst.apply_subst subst t2 in