Let x0 of type ι → ι → ι be given.

Assume H0: (λ x1 x2 . x0 x2 x1) = ChurchBoolFal.

Assume H1: x0 = ChurchBoolFal.

Apply unknownprop_2a02b07cb2d1646750378f6f1ee4d840c838599ffd77846a5a2b747d49a8a268.

Apply H0 with λ x1 x2 : ι → ι → ι . ChurchBoolTru = x1.

Apply H1 with λ x1 x2 : ι → ι → ι . ChurchBoolTru = λ x3 x4 . x2 x4 x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H2: x1 ChurchBoolTru (λ x2 x3 . ChurchBoolFal x3 x2).

The subproof is completed by applying H2.

■

Proofgold Proof