Let x0 of type ο be given.
Assume H0:
∀ x1 : ι → ι → ο . (∀ x2 : ο . ((∀ x3 x4 . x1 x3 x4 ⟶ x1 x4 x3) ⟶ x1 0 1 ⟶ x1 1 2 ⟶ x1 2 3 ⟶ x1 3 4 ⟶ x1 4 0 ⟶ not (x1 0 2) ⟶ not (x1 0 3) ⟶ not (x1 1 3) ⟶ not (x1 1 4) ⟶ not (x1 2 4) ⟶ x2) ⟶ x2) ⟶ x0.
Apply H0 with
λ x1 x2 . or (or (or (or (and (x1 = 0) (or (x2 = 4) (x2 = 1))) (and (x1 = 1) (or (x2 = 0) (x2 = 2)))) (and (x1 = 2) (or (x2 = 1) (x2 = 3)))) (and (x1 = 3) (or (x2 = 2) (x2 = 4)))) (and (x1 = 4) (or (x2 = 3) (x2 = 0))).
Let x1 of type ο be given.
Assume H1:
... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ not ((λ x2 x3 . or (or (or (or (and (x2 = 0) (or (x3 = 4) (x3 = 1))) (and (x2 = 1) (or (x3 = 0) (x3 = 2)))) (and (x2 = 2) (or (x3 = 1) (x3 = 3)))) (and (x2 = 3) ...)) ...) 1 3) ⟶ not ((λ x2 x3 . or (or (or (or (and (x2 = 0) (or (x3 = 4) (x3 = 1))) (and (x2 = 1) (or (x3 = 0) (x3 = 2)))) (and (x2 = 2) (or (x3 = 1) (x3 = 3)))) (and (x2 = 3) (or (x3 = 2) (x3 = 4)))) (and (x2 = 4) (or (x3 = 3) (x3 = 0)))) 1 4) ⟶ not ((λ x2 x3 . or (or (or (or (and (x2 = 0) (or (x3 = 4) (x3 = 1))) (and (x2 = 1) (or (x3 = 0) (x3 = 2)))) (and (x2 = 2) (or (x3 = 1) (x3 = 3)))) (and (x2 = 3) (or (x3 = 2) (x3 = 4)))) (and (x2 = 4) (or (x3 = 3) (x3 = 0)))) 2 4) ⟶ x1.