Apply unknownprop_4a8fb8184a9382c55bc8b80e50037d60f4917ee0a833018fbdeae085ab757aab with
λ x0 . Union (ordsucc x0) = x0.
Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Union (ordsucc x0),
x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with
ordsucc x0,
x1,
In x1 x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x2,
x0,
x1 leaving 2 subgoals.
Apply unknownprop_b6cc2d63af54c19d89079177eacbb5d21c63c324fc4fe29c2940b0c234644bed with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with
ordsucc x0,
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.