| ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ or ((λ x2 x3 . x0 x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) = λ x2 x3 . x2) ((λ x2 x3 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x2 x2) = λ x2 x3 . x2) |
|