Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι be given.
Assume H0: fb516.. x0.
Apply H0 with 6fb7f.. (permargs_i_1_0 x0) = not (6fb7f.. x0) leaving 2 subgoals.
Assume H1: x0 = ChurchBoolTru.
Apply H1 with λ x1 x2 : ι → ι → ι . 6fb7f.. (permargs_i_1_0 x2) = not (6fb7f.. x2).
Apply prop_ext_2 with 6fb7f.. ChurchBoolFal, not (6fb7f.. ChurchBoolTru) leaving 2 subgoals.
Assume H2: 6fb7f.. ChurchBoolFal.
The subproof is completed by applying unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.
Assume H2: not (6fb7f.. ChurchBoolTru).
The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.
Assume H1: x0 = ChurchBoolFal.
Apply H1 with λ x1 x2 : ι → ι → ι . 6fb7f.. (permargs_i_1_0 x2) = not (6fb7f.. x2).
Apply prop_ext_2 with 6fb7f.. ChurchBoolTru, not (6fb7f.. ChurchBoolFal) leaving 2 subgoals.
Assume H2: 6fb7f.. ChurchBoolTru.
Apply FalseE with not (6fb7f.. ChurchBoolFal).
Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.
The subproof is completed by applying H2.
Assume H2: not (6fb7f.. ChurchBoolFal).
Apply FalseE with 6fb7f.. ChurchBoolTru.
Apply H2.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H3: x1 ChurchBoolFal ChurchBoolFal.
The subproof is completed by applying H3.
■