Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with
λ x0 x1 . nat_p x0.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with
2,
5 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_5.