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