Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x2 . In (add_nat x1 x2) (add_nat x0 x2) leaving 2 subgoals.
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
x1,
λ x2 x3 . In x3 (add_nat x0 0).
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
x0,
λ x2 x3 . In x1 x3.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_bfc870f6d786cc78805c5bf0f9864161d18f532f6daf7daf1d02f4a58dac06f9 with
x1,
x2,
λ x3 x4 . In x4 (add_nat x0 (ordsucc x2)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_bfc870f6d786cc78805c5bf0f9864161d18f532f6daf7daf1d02f4a58dac06f9 with
x0,
x2,
λ x3 x4 . In (ordsucc (add_nat x1 x2)) x4 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_3336121954edce0fefb5edee2ad1b426a9827aac09625122db0ff807b493dc73 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_2539815e221739e5ed231d021c9e8622ca0ca73d6737f4a44b47896fd145c3c2 with
add_nat x0 x2,
add_nat x1 x2 leaving 2 subgoals.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
add_nat x0 x2.
The subproof is completed by applying L4.
The subproof is completed by applying H3.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In (ordsucc (add_nat x1 x2)) (add_nat x0 x2),
add_nat x0 x2 = ordsucc (add_nat x1 x2),
In (ordsucc (add_nat x1 x2)) (ordsucc (add_nat x0 x2)) leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying unknownprop_9d1f2833af10907d78259d2045ff2d1e1026643f459cca4199c4ae7f89385ba4 with
add_nat x0 x2,
ordsucc (add_nat x1 x2).
Apply H6 with
λ x3 x4 . In (ordsucc (add_nat x1 x2)) (ordsucc x4).
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with
ordsucc (add_nat x1 x2).