Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι be given.
Apply unknownprop_b9e706605ee9588d251c289fbb55bc905fa3eb7fe1a8560e3057c9742d5adef0 with
λ x5 x6 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ο . binop_on x0 x1 ⟶ binop_on x0 x2 ⟶ binop_on x0 x3 ⟶ (∀ x7 . In x7 x0 ⟶ and (x1 x4 x7 = x7) (x1 x7 x4 = x7)) ⟶ (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ and (and (and (x2 x7 (x1 x7 x8) = x8) (x1 x7 (x2 x7 x8) = x8)) (x3 (x1 x7 x8) x8 = x7)) (x1 (x3 x7 x8) x8 = x7)) ⟶ x6 x0 x1 x2 x3 x4.
The subproof is completed by applying unknownprop_9b09b99fce48fbc4294fba4077c15371ba18b57a0bc4e20cfa1cf1c48cd99108 with
binop_on x0 x1,
binop_on x0 x2,
binop_on x0 x3,
∀ x5 . In x5 x0 ⟶ and (x1 x4 x5 = x5) (x1 x5 x4 = x5),
∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ and (and (and (x2 x5 (x1 x5 x6) = x6) (x1 x5 (x2 x5 x6) = x6)) (x3 (x1 x5 x6) x6 = x5)) (x1 (x3 x5 x6) x6 = x5).