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 6fb7f.. (efcd0.. x0 x1) = (6fb7f.. x0 ⟶ 6fb7f.. x1) leaving 2 subgoals.
Assume H2: x0 = ChurchBoolTru.
Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (efcd0.. x3 x1) = (6fb7f.. x3 ⟶ 6fb7f.. x1).
Apply prop_ext_2 with 6fb7f.. ChurchBoolFal, 6fb7f.. ChurchBoolTru ⟶ 6fb7f.. x1 leaving 2 subgoals.
Assume H3: 6fb7f.. ChurchBoolFal.
Assume H4: 6fb7f.. ChurchBoolTru.
Apply FalseE with 6fb7f.. x1.
Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.
The subproof is completed by applying H4.
Assume H3: 6fb7f.. ChurchBoolTru ⟶ 6fb7f.. x1.
The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.
Assume H2: x0 = ChurchBoolFal.
Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (efcd0.. x3 x1) = (6fb7f.. x3 ⟶ 6fb7f.. x1).
Apply unknownprop_fe36caae5784dcaccf90e3c33c4c3db05a48fc46bf7e1321a13b032e9121e798 with λ x2 x3 : ι → ι → ι . 6fb7f.. (efcd0.. x3 x1) = (6fb7f.. x3 ⟶ 6fb7f.. x1).
Apply prop_ext_2 with 6fb7f.. x1, 6fb7f.. ChurchBoolFal ⟶ 6fb7f.. x1 leaving 2 subgoals.
Assume H3: 6fb7f.. x1.
Assume H4: 6fb7f.. ChurchBoolFal.
The subproof is completed by applying H3.
Assume H3: 6fb7f.. ChurchBoolFal ⟶ 6fb7f.. x1.
Apply H3.
The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.
■