Apply unknownprop_0ab0f3bd8351c27d763063f15ec4b3e9dd38d8c64505f2de3a82cb8384f460b9 with
λ x0 x1 . 24 ∈ ordsucc x0.
Apply unknownprop_65854e80dcdfdaad216d9278c1826bfa6e412eacf7818f3d49e43d93a23f7bcf with
24,
7.
The subproof is completed by applying nat_7.