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

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

Assume H0: fb516.. x0.

Assume H1: fb516.. x1.

Apply H0 with 6fb7f.. (cc64c.. x0 x1) = and (6fb7f.. x0) (6fb7f.. x1) leaving 2 subgoals.

Assume H2: x0 = ChurchBoolTru.

Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (cc64c.. x3 x1) = and (6fb7f.. x3) (6fb7f.. x1).

Apply prop_ext_2 with 6fb7f.. ChurchBoolTru, and (6fb7f.. ChurchBoolTru) (6fb7f.. x1) leaving 2 subgoals.

Assume H3: 6fb7f.. ChurchBoolTru.

Apply FalseE with and (6fb7f.. ChurchBoolTru) (6fb7f.. x1).

Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.

The subproof is completed by applying H3.

Assume H3: and (6fb7f.. ChurchBoolTru) (6fb7f.. x1).

Apply FalseE with 6fb7f.. ChurchBoolTru.

Apply H3 with False.

Assume H4: 6fb7f.. ChurchBoolTru.

Assume H5: 6fb7f.. x1.

Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.

The subproof is completed by applying H4.

Assume H2: x0 = ChurchBoolFal.

Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (cc64c.. x3 x1) = and (6fb7f.. x3) (6fb7f.. x1).

Apply unknownprop_fe36caae5784dcaccf90e3c33c4c3db05a48fc46bf7e1321a13b032e9121e798 with λ x2 x3 : ι → ι → ι . 6fb7f.. (cc64c.. x3 x1) = and (6fb7f.. x3) (6fb7f.. x1).

Apply prop_ext_2 with 6fb7f.. x1, and (6fb7f.. ChurchBoolFal) (6fb7f.. x1) leaving 2 subgoals.

Assume H3: 6fb7f.. x1.

Apply andI with 6fb7f.. ChurchBoolFal, 6fb7f.. x1 leaving 2 subgoals.

The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.

The subproof is completed by applying H3.

Assume H3: and (6fb7f.. ChurchBoolFal) (6fb7f.. x1).

Apply H3 with 6fb7f.. x1.

Assume H4: 6fb7f.. ChurchBoolFal.

Assume H5: 6fb7f.. x1.

The subproof is completed by applying H5.

■

Proofgold Proof