Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with
λ x0 x1 . 17 ∈ x0.
Apply unknownprop_18dab10013860d442d73fc2b55cfee57e61b2e3044d2d0c29767dba9e5eb2112 with
λ x0 x1 . ordsucc x0 ∈ exp_nat 2 5.
Apply unknownprop_441f51eac9a2dfe161ce38a8744a6c32b2686e6c04076ec100ae43cffb074cd3 with
3.
The subproof is completed by applying nat_3.