Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
V_ (ordsucc x0),
Power (V_ x0) leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_3687558d9284fdd514174bfe87bba39032212334a6409eb4554d4077dea6d831 with
x1,
ordsucc x0,
In x1 (Power (V_ x0)) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
V_ x0,
x1.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x0,
x2,
Subq x1 (V_ x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_9143b3674c790ed26c1d41216fe3742a8002230ba5cffca45c4cf28cb75c4718 with
x2,
x0.
Apply unknownprop_5af24edc592c6d7fa3cf53e40211635bbed8f39380469ac8aef3490ee700739c with
V_ x0,
x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_246dbbaa90a30a59bb82c977db3a76b865348aa516921f45ddd5a06925460ee4 with x0.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
x2,
x2,
x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying unknownprop_e77e4bcf720b10eb052a18cf9f6bcfdab55679bfac74fe7d30864c1712a56341 with x2.
Apply unknownprop_16d2e0ac4e61f9d6f4710f68fd29bc0751fdb2a43ae4ee41dc39565d6502f8a7 with
x1,
V_ x2,
V_ x0 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Assume H4: x2 = x0.
Apply H4 with
λ x3 x4 . Subq x1 (V_ x3).
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply unknownprop_a2c3fca2e8c461af2fcd2014916bc97ec486da998a233beedf90ec14d6bf2e76 with
x1,
x0,
ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.
Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with
V_ x0,
x1.
The subproof is completed by applying H1.