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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι → ι → ι be given.
Apply H0 with
MetaCat_equalizer_buggy_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x5 x4 x6 x7 x8 x9 x10.
Assume H1:
and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x5 x8 x9).
Apply H1 with
(∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12)) ⟶ MetaCat_equalizer_buggy_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x5 x4 x6 x7 x8 x9 x10.
Assume H2:
and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8).
Apply H2 with
x1 x5 x8 x9 ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12)) ⟶ MetaCat_equalizer_buggy_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x5 x4 x6 x7 x8 x9 x10.
Assume H3:
and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 ... ...).