Let x0 of type ι be given.
Apply unknownprop_8acfb80b309c166e5c3c41e4a1cc49c4ea05db3f03d215384dabecf7c22c27a2 with
x0,
λ x1 x2 . minus_SNo x0 = ad280.. (minus_SNo x2) (minus_SNo (d634d.. x0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_2a9fa88c4206964d15bfbbc297f8b3b39425bd997c7d45b304d4d13c3943fd64 with
x0,
λ x1 x2 . minus_SNo x0 = ad280.. (minus_SNo x0) (minus_SNo x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply minus_SNo_0 with
λ x1 x2 . minus_SNo x0 = ad280.. (minus_SNo x0) x2.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying unknownprop_872273e895264b163d3a3b042c5d1abf262e26919401a643ccce2dcdcb6a14ef with
minus_SNo x0,
λ x2 x3 . x1 x3 x2.