Apply add_SNo_cancel_R with
add_SNo u24 (minus_SNo u20),
u20,
u4 leaving 4 subgoals.
Apply SNo_add_SNo with
u24,
minus_SNo u20 leaving 2 subgoals.
Apply nat_p_SNo with
u24.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply SNo_minus_SNo with
u20.
Apply nat_p_SNo with
u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_SNo with
u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_SNo with
u4.
The subproof is completed by applying nat_4.
Apply add_SNo_minus_R2' with
u24,
u20,
λ x0 x1 . x1 = add_SNo u4 u20 leaving 3 subgoals.
Apply nat_p_SNo with
u24.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply nat_p_SNo with
u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Let x0 of type ι → ι → ο be given.
Apply add_SNo_com with
u4,
u20,
λ x1 x2 . x2 = u24,
λ x1 x2 . x0 x2 x1 leaving 3 subgoals.
Apply nat_p_SNo with
u4.
The subproof is completed by applying nat_4.
Apply nat_p_SNo with
u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply add_nat_add_SNo with
u20,
u4,
λ x1 x2 . x1 = u24 leaving 3 subgoals.
Apply nat_p_omega with
u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_omega with
u4.
The subproof is completed by applying nat_4.
The subproof is completed by applying unknownprop_e7a22d56172b83cc5d886239f486a15dd72ae38e01e724bdd7d4045095e9b394.