Gro-Tsen is just defining x<n> recursively. "by induction" there doesn't mean "proof by induction".