Let x0 of type ι → ι → ο be given.
Apply H0 with
partialorder (reflclos x0).
Apply and3I with
reflexive (reflclos x0),
antisymmetric (reflclos x0),
transitive (reflclos x0) leaving 3 subgoals.
The subproof is completed by applying reflclos_refl with x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H3:
or (x0 x1 x2) (x1 = x2).
Assume H4:
or (x0 x2 x1) (x2 = x1).
Apply H3 with
x1 = x2 leaving 2 subgoals.
Assume H5: x0 x1 x2.
Apply H4 with
x1 = x2 leaving 2 subgoals.
Assume H6: x0 x2 x1.
Apply FalseE with
x1 = x2.
Claim L7: x0 x1 x1
Apply H2 with
x1,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply H1 with
x1.
The subproof is completed by applying L7.
Assume H6: x2 = x1.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H6 with λ x4 x5 . x3 x5 x4.
Assume H5: x1 = x2.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H3:
or (x0 x1 x2) (x1 = x2).
Assume H4:
or (x0 x2 x3) (x2 = x3).
Apply H3 with
or (x0 x1 x3) (x1 = x3) leaving 2 subgoals.
Assume H5: x0 x1 x2.
Apply H4 with
or (x0 x1 x3) (x1 = x3) leaving 2 subgoals.
Assume H6: x0 x2 x3.
Apply orIL with
x0 x1 x3,
x1 = x3.
Apply H2 with
x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H6: x2 = x3.
Apply orIL with
x0 x1 x3,
x1 = x3.
Apply H6 with
λ x4 x5 . x0 x1 x4.
The subproof is completed by applying H5.
Assume H5: x1 = x2.
Apply H4 with
or (x0 x1 x3) (x1 = x3) leaving 2 subgoals.
Assume H6: x0 x2 x3.
Apply orIL with
x0 x1 x3,
x1 = x3.
Apply H5 with
λ x4 x5 . x0 x5 x3.
The subproof is completed by applying H6.
Assume H6: x2 = x3.
Apply orIR with
x0 x1 x3,
x1 = x3.
Apply H6 with
λ x4 x5 . x1 = x4.
The subproof is completed by applying H5.