Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (ι → ι → ι) → ι → ι → ι be given.
Assume H0: ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1).
Apply unknownprop_3b229b9e11502aa649ddc1c912619ddb1c48e5eed9d2f5f044b1a524ed6e72b2 with x0 ChurchBoolTru, x0 ChurchBoolFal leaving 2 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.
■