Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_7750078cf23be1c80f04c25ad7cbaaf73ac1b6c9f1f54ab639cc8621b4808d18 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In (ordsucc x1) x0,
Subq x0 (ordsucc x1),
In (ordsucc x1) (ordsucc x0) leaving 3 subgoals.
Apply unknownprop_682983ef060476485fcd03b6da6255e287c5314c9013030e2a8b79c1fa302a8c with
ordsucc x1,
x0 leaving 2 subgoals.
Apply unknownprop_ebe0d24cdae5bc4d34287c45ae7c3f85ae6f87f22e9e02dfbb80c201dccf4414 with
x1.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
ordsucc x0,
ordsucc x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b2bebb8105f29e822888ab2d4b10db11282fc91a7326e3993f508ffc07b3af08 with x0.
The subproof is completed by applying H3.
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
ordsucc x1,
x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
Apply L4 with
λ x2 x3 . In x3 (ordsucc x0).
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.