Search for blocks/addresses/...

Proofgold Proof

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