Let x0 of type ι be given.
Let x1 of type ι be given.
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.
Apply unknownprop_497ef0b809178e9ac674acf0f41f994a7e76b824de0430efd934f6540a71daab with
x0,
ordsucc x1,
or (In (ordsucc x1) x0) (x0 = ordsucc x1) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L2.
Apply FalseE with
or (In (ordsucc x1) x0) (x0 = ordsucc x1).
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
x1,
x0,
False leaving 3 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_7aafb642c31e9be85457ec0eb47aa596cd38ae4297ed5252dc50af56ee6c9208 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Assume H4: x0 = x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x0,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c08c2271cf6ba0885c1e030cb2abcd9decbf5e7798ef2ffc9064daf191c9f920 with x0.
Apply H4 with
λ x2 x3 . In x3 x0.
The subproof is completed by applying H1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
In (ordsucc x1) x0,
x0 = ordsucc x1.
The subproof is completed by applying H3.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
In (ordsucc x1) x0,
x0 = ordsucc x1.
The subproof is completed by applying H3.