consider m being Nat such that
B0: Depth phi = m + 1 by NAT_1:6;
consider phi2 being m -wff string of S such that
B1: tail phi = phi2 by B0, Lm49;
thus tail phi is wff string of S by B1; :: thesis: verum