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 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ο . x6 x0 x1 x2 x3 x4 ⟶ ∀ x7 : ο . (binop_on x0 x1 ⟶ binop_on x0 x2 ⟶ binop_on x0 x3 ⟶ (∀ x8 . In x8 x0 ⟶ and (x1 x4 x8 = x8) (x1 x8 x4 = x8)) ⟶ (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ and (and (and (x2 x8 (x1 x8 x9) = x9) (x1 x8 (x2 x8 x9) = x9)) (x3 (x1 x8 x9) x9 = x8)) (x1 (x3 x8 x9) x9 = x8)) ⟶ x7) ⟶ x7.
The subproof is completed by applying unknownprop_bcfb235173b6e24d61b0900ebc9059688ec23fd5128404d7a36e3b666224a280 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).