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