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

Assume H0: ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1).

Apply unknownprop_dc639444341820cc8ac415204064e1686ba12f18cf7044b00dab38d1f90436e3 with x0 ChurchBoolTru, x0 ChurchBoolFal, λ x1 x2 : ο . x2 = ∃ x3 : ι → ι → ι . and (fb516.. x3) (6fb7f.. (x0 x3)) leaving 3 subgoals.

Apply H0 with ChurchBoolTru.

The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.

Apply H0 with ChurchBoolFal.

The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.

Apply prop_ext_2 with or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)), ∃ x1 : ι → ι → ι . and (fb516.. x1) (6fb7f.. (x0 x1)) leaving 2 subgoals.

Assume H1: or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).

Apply H1 with ∃ x1 : ι → ι → ι . and (fb516.. x1) (6fb7f.. (x0 x1)) leaving 2 subgoals.

Assume H2: 6fb7f.. (x0 ChurchBoolTru).

Let x1 of type ο be given.

Assume H3: ∀ x2 : ι → ι → ι . and (fb516.. x2) (6fb7f.. (x0 x2)) ⟶ x1.

Apply H3 with ChurchBoolTru.

Apply andI with fb516.. ChurchBoolTru, 6fb7f.. (x0 ChurchBoolTru) leaving 2 subgoals.

The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.

The subproof is completed by applying H2.

Assume H2: 6fb7f.. (x0 ChurchBoolFal).

Let x1 of type ο be given.

Assume H3: ∀ x2 : ι → ι → ι . and (fb516.. x2) (6fb7f.. (x0 x2)) ⟶ x1.

Apply H3 with ChurchBoolFal.

Apply andI with fb516.. ChurchBoolFal, 6fb7f.. (x0 ChurchBoolFal) leaving 2 subgoals.

The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.

The subproof is completed by applying H2.

Assume H1: ∃ x1 : ι → ι → ι . and (fb516.. x1) (6fb7f.. (x0 x1)).

Apply H1 with or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).

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

Assume H2: (λ x2 : ι → ι → ι . and (fb516.. x2) (6fb7f.. (x0 x2))) x1.

Apply H2 with or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).

Assume H3: fb516.. x1.

Apply H3 with 6fb7f.. (x0 x1) ⟶ or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)) leaving 2 subgoals.

Assume H4: x1 = ChurchBoolTru.

Apply H4 with λ x2 x3 : ι → ι → ι . 6fb7f.. (x0 x3) ⟶ or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).

The subproof is completed by applying orIL with 6fb7f.. (x0 ChurchBoolTru), 6fb7f.. (x0 ChurchBoolFal).

Assume H4: x1 = ChurchBoolFal.

Apply H4 with λ x2 x3 : ι → ι → ι . 6fb7f.. (x0 x3) ⟶ or (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).

The subproof is completed by applying orIR with 6fb7f.. (x0 ChurchBoolTru), 6fb7f.. (x0 ChurchBoolFal).

■

Proofgold Proof