Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι be given.
Let x1 of type ι → ι → ι be given.
Assume H0: fb516.. x0.
Assume H1: fb516.. x1.
Apply H0 with fb516.. (c2beb.. x0 x1) leaving 2 subgoals.
Assume H2: x0 = ChurchBoolTru.
Apply H2 with λ x2 x3 : ι → ι → ι . fb516.. (c2beb.. x3 x1).
Apply unknownprop_af7df763fd0193d8c3e3722c850a73ec398ea041c70f9eb9b8651624239a4375 with λ x2 x3 : ι → ι → ι . fb516.. (c2beb.. x3 x1).
The subproof is completed by applying H1.
Assume H2: x0 = ChurchBoolFal.
Apply H2 with λ x2 x3 : ι → ι → ι . fb516.. (c2beb.. x3 x1).
Apply unknownprop_fe36caae5784dcaccf90e3c33c4c3db05a48fc46bf7e1321a13b032e9121e798 with λ x2 x3 : ι → ι → ι . fb516.. x3.
The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.
■