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 t1 = CicMetaSubst.apply_subst subst t1 in
let t2 = CicMetaSubst.apply_subst subst t2 in
let ty = CicMetaSubst.apply_subst subst ty in