Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_5e27941980fd82e6bd970186ba0607de8244696a96acf12736011288a143d4ba with
x0,
x1,
or (099f3.. x0 x1) (fe4bb.. x1 x0) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with
or (099f3.. x0 x1) (fe4bb.. x1 x0) leaving 2 subgoals.
Apply orIL with
099f3.. x0 x1,
fe4bb.. x1 x0.
The subproof is completed by applying H3.
Assume H3: x0 = x1.
Apply orIR with
099f3.. x0 x1,
fe4bb.. x1 x0.
Apply H3 with
λ x2 x3 . fe4bb.. x1 x3.
The subproof is completed by applying unknownprop_f017f6ee910dd235f4bf08afbbbf148d42e1360d8b1094fb435baedbfe8b2ac8 with x1.
Apply orIR with
099f3.. x0 x1,
fe4bb.. x1 x0.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
x1,
x0.
The subproof is completed by applying H2.