Let x0 of type ι → ι → ο be given.
Apply H0 with
totalorder (reflclos x0).
Apply andI with
partialorder (reflclos x0),
linear (reflclos x0) leaving 2 subgoals.
Apply strictpartialorder_partialorder_reflclos with
x0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply or3E with
x0 x1 x2,
x1 = x2,
x0 x2 x1,
or (or (x0 x1 x2) (x1 = x2)) (or (x0 x2 x1) (x2 = x1)) leaving 4 subgoals.
The subproof is completed by applying H2 with x1, x2.
Assume H3: x0 x1 x2.
Apply orIL with
or (x0 x1 x2) (x1 = x2),
or (x0 x2 x1) (x2 = x1).
Apply orIL with
x0 x1 x2,
x1 = x2.
The subproof is completed by applying H3.
Assume H3: x1 = x2.
Apply orIL with
or (x0 x1 x2) (x1 = x2),
or (x0 x2 x1) (x2 = x1).
Apply orIR with
x0 x1 x2,
x1 = x2.
The subproof is completed by applying H3.
Assume H3: x0 x2 x1.
Apply orIR with
or (x0 x1 x2) (x1 = x2),
or (x0 x2 x1) (x2 = x1).
Apply orIL with
x0 x2 x1,
x2 = x1.
The subproof is completed by applying H3.