if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)
if does_not_occur 1 t_typ then
(* since [Rel 1] does not occur in typ, substituting any term *)
(* in place of [Rel 1] is equivalent to delifting once *)