Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3.
Apply unknownprop_6cb16650b83c24e67a3a0331297883371adfe848666ffd004f11baa09cc883b5 with
051a7.. (λ x2 x3 . or (x0 x2 x3) (1ca3e.. x2 x3)),
051a7.. (λ x2 x3 . or (x1 x2 x3) (1ca3e.. x2 x3)).
Apply unknownprop_98f7d80acf8671d0b6562fee5e18618b2141ec3dd100bb8db1ac3e3e5331582c with
λ x2 x3 . or (x0 x2 x3) (1ca3e.. x2 x3),
λ x2 x3 . or (x1 x2 x3) (1ca3e.. x2 x3).
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply H1 with
or (x1 x2 x3) (1ca3e.. x2 x3) leaving 2 subgoals.
Assume H2: x0 x2 x3.
Apply orIL with
x1 x2 x3,
1ca3e.. x2 x3.
Apply H0 with
x2,
x3.
The subproof is completed by applying H2.
Apply orIR with
x1 x2 x3,
1ca3e.. x2 x3.
The subproof is completed by applying H2.