Apply unknownprop_e5d031cf873471b22fe77dee36ebb6254dbd5df83fe741afd4ca8450323be464 with
u12,
λ x0 x1 . x1 = u24 leaving 2 subgoals.
Apply nat_p_SNo with
u12.
The subproof is completed by applying nat_12.
Apply add_nat_add_SNo with
u12,
u12,
λ x0 x1 . x0 = u24 leaving 3 subgoals.
Apply nat_p_omega with
u12.
The subproof is completed by applying nat_12.
Apply nat_p_omega with
u12.
The subproof is completed by applying nat_12.
The subproof is completed by applying unknownprop_6e7cb10edc0b40043a252508d525ece5fdeb3d7816f12ce145ff850cf21c79ba.