Apply unknownprop_4a8fb8184a9382c55bc8b80e50037d60f4917ee0a833018fbdeae085ab757aab with
λ x0 . Inj1 x0 = ordsucc x0.
Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Inj1 x0,
ordsucc x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_0b120035bc22426ea02988561990499be78ef89e658ec0c0b4bcff54639930cb with
x0,
x1,
λ x2 . In x2 (ordsucc x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_7612098ac051ddb44a738cd26605b0533c4bf20733169dbdc9a2d3797ceb4f30 with
x0.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply H1 with
x2,
λ x3 x4 . In x4 (ordsucc x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_a8f766a07ce4037c1a1cdb7512a4eb008ff74917c7385d889b7b933b3b099900 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x0,
x1,
In x1 (Inj1 x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
x1 = 0,
∃ x2 . and (nat_p x2) (x1 = ordsucc x2),
In x1 (Inj1 x0) leaving 3 subgoals.
Apply unknownprop_7be30b7cfc1f28933d3b9926f9200a8d420af1a2342269d520eb5a249c6f8c26 with
x1.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Assume H4: x1 = 0.
Apply H4 with
λ x2 x3 . In x3 (Inj1 x0).
The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x0.
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with
nat_p,
λ x2 . x1 = ordsucc x2,
In x1 (Inj1 x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply H6 with
λ x3 x4 . In x4 (Inj1 x0).
Apply H6 with
λ x3 x4 . In x2 x4.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x1,
x0,
x2 leaving 2 subgoals.
Apply unknownprop_92b4103b83752522eb6c235601eefa2912e3f6395a346e3a7eb52bb5e37ede81 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L7.
Apply H1 with
x2,
λ x3 x4 . In x3 (Inj1 x0) leaving 2 subgoals.
The subproof is completed by applying L8.
Apply unknownprop_20467f36510c7b6830c7e44d6955dc079b6e83b8bbc05b0500ccb9075a391641 with
x0,
x2.
The subproof is completed by applying L8.
Assume H3: x1 = x0.
Apply H3 with
λ x2 x3 . In x3 (Inj1 x0).
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
x0 = 0,
∃ x2 . and (nat_p x2) (x0 = ordsucc x2),
In x0 (Inj1 x0) leaving 3 subgoals.
Apply unknownprop_7be30b7cfc1f28933d3b9926f9200a8d420af1a2342269d520eb5a249c6f8c26 with
x0.
The subproof is completed by applying H0.
Assume H4: x0 = 0.
Apply H4 with
λ x2 x3 . In x3 (Inj1 x0).
The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x0.
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with
nat_p,
λ x2 . x0 = ordsucc x2,
In x0 (Inj1 x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply H6 with
λ x3 x4 . In x4 (Inj1 x0).
Apply H6 with
λ x3 x4 . In x2 x4.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x2.
Apply H1 with
x2,
λ x3 x4 . In x3 (Inj1 x0) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_20467f36510c7b6830c7e44d6955dc079b6e83b8bbc05b0500ccb9075a391641 with
x0,
x2.
The subproof is completed by applying L7.
Let x0 of type ι be given.
Apply unknownprop_8438e883de7a1eeb39e847b7d0ce5ef143abdad5f0a5010ee69558812716e137 with
x0,
λ x1 x2 . x2 = ordsucc x0.
Apply L0 with
x0.
The subproof is completed by applying H1.