Apply unknownprop_1a8ef7119409201047d8cb04fc57c6c2b31fe9c149f99c6d6378838840c55565 with
λ x0 x1 . 23 ∈ ordsucc x0.
Apply unknownprop_65854e80dcdfdaad216d9278c1826bfa6e412eacf7818f3d49e43d93a23f7bcf with
23,
8.
The subproof is completed by applying nat_8.