pf |
---|
Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with λ x0 . ∀ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (In x0 x1) (x0 = x1)) (In x1 x0).
Let x0 of type ι be given.
Assume H0: ∀ x1 . In x1 x0 ⟶ ∀ x2 . ordinal x1 ⟶ ordinal x2 ⟶ or (or (In x1 x2) (x1 = x2)) (In x2 x1).
Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with λ x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (In x0 x1) (x0 = x1)) (In x1 x0).
Let x1 of type ι be given.
Apply unknownprop_80056f9db85f84f8ce0644e1cdb62f5e66ec62c041f28dd7a07b3c46de1ea696 with x0, x1, or (or (In x0 x1) (x0 = x1)) (In x1 x0) leaving 2 subgoals.
Apply unknownprop_0e1ba7291a295ea3c1979b40483f7544221790d53d76aadba99638689b88d9d1 with In x0 x1, x0 = x1, In x1 x0.
The subproof is completed by applying H4.
Apply unknownprop_80056f9db85f84f8ce0644e1cdb62f5e66ec62c041f28dd7a07b3c46de1ea696 with x1, x0, or (or (In x0 x1) (x0 = x1)) (In x1 x0) leaving 2 subgoals.
Apply unknownprop_c33a8518d3fc8314286e0e0f7acdb4e408d0225cb1257a73db3a51552718bbdd with In x0 x1, x0 = x1, In x1 x0.
The subproof is completed by applying H5.
Apply unknownprop_55d33d10f6a09aaaea8e002117cf1820d9dc4418a57f04c18d4ec79694021a99 with In x0 x1, x0 = x1, In x1 x0.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with x0, x1 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with In x2 x1, x2 = x1, In x1 x2, In x2 x1 leaving 4 subgoals.
Apply H0 with x2, x1 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L7.
The subproof is completed by applying H3.
The subproof is completed by applying H8.
Assume H8: x2 = x1.
Apply FalseE with In x2 x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply H8 with λ x3 x4 . In x3 x0.
The subproof is completed by applying H6.
Apply FalseE with In x2 x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_16d203cf35db7c43083950b8cdf3bc14c48faba5d53a8b40d54b8c3e00a23527 with x0, x2, x1 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with In x0 x2, x0 = x2, In x2 x0, In x2 x0 leaving 4 subgoals.
Apply H1 with x2 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
The subproof is completed by applying L7.
Apply FalseE with In x2 x0.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_16d203cf35db7c43083950b8cdf3bc14c48faba5d53a8b40d54b8c3e00a23527 with x1, x2, x0 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Assume H8: x0 = x2.
Apply FalseE with In x2 x0.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply H8 with λ x3 x4 . In x4 x1.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
■
|
|