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.. (355fd.. x0 x1) = iff (6fb7f.. x0) (6fb7f.. x1) leaving 2 subgoals.
Assume H2: x0 = ChurchBoolTru.
Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (355fd.. x3 x1) = iff (6fb7f.. x3) (6fb7f.. x1).
Apply unknownprop_22313e17c4c59d6d8dbe2958633ad6b7e623ac8998f7980148e06205729b37b4 with x1, λ x2 x3 : ο . x3 = iff (6fb7f.. ChurchBoolTru) (6fb7f.. x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply prop_ext_2 with not (6fb7f.. x1), iff (6fb7f.. ChurchBoolTru) (6fb7f.. x1) leaving 2 subgoals.
Assume H3: not (6fb7f.. x1).
Apply iffI with 6fb7f.. ChurchBoolTru, 6fb7f.. x1 leaving 2 subgoals.
Assume H4: 6fb7f.. ChurchBoolTru.
Apply FalseE with 6fb7f.. x1.
Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.
The subproof is completed by applying H4.
Assume H4: 6fb7f.. x1.
Apply FalseE with 6fb7f.. ChurchBoolTru.
Apply H3.
The subproof is completed by applying H4.
Assume H3: iff (6fb7f.. ChurchBoolTru) (6fb7f.. x1).
Assume H4: 6fb7f.. x1.
Apply H3 with False.
Assume H5: 6fb7f.. ChurchBoolTru ⟶ 6fb7f.. x1.
Assume H6: 6fb7f.. x1 ⟶ 6fb7f.. ChurchBoolTru.
Apply unknownprop_4db3dccc9d2b781cbc51e143c21b1ce8ea7a94ab506258592ed1c524bf6deaea.
Apply H6.
The subproof is completed by applying H4.
Assume H2: x0 = ChurchBoolFal.
Apply H2 with λ x2 x3 : ι → ι → ι . 6fb7f.. (355fd.. x3 x1) = iff (6fb7f.. x3) (6fb7f.. x1).
Apply unknownprop_fe36caae5784dcaccf90e3c33c4c3db05a48fc46bf7e1321a13b032e9121e798 with λ x2 x3 : ι → ι → ι . 6fb7f.. (355fd.. x3 x1) = iff (6fb7f.. ChurchBoolFal) (6fb7f.. x1).
Apply prop_ext_2 with 6fb7f.. x1, iff (6fb7f.. ChurchBoolFal) (6fb7f.. x1) leaving 2 subgoals.
Assume H3: 6fb7f.. x1.
Apply iffI with 6fb7f.. ChurchBoolFal, 6fb7f.. x1 leaving 2 subgoals.
Assume H4: 6fb7f.. ChurchBoolFal.
The subproof is completed by applying H3.
Assume H4: 6fb7f.. x1.
The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.
Assume H3: iff (6fb7f.. ChurchBoolFal) (6fb7f.. x1).
Apply H3 with 6fb7f.. x1.
Assume H4: 6fb7f.. ChurchBoolFal ⟶ 6fb7f.. x1.
Assume H5: 6fb7f.. x1 ⟶ 6fb7f.. ChurchBoolFal.
Apply H4.
The subproof is completed by applying unknownprop_c16a7e66d013fefc3e2d9d08fe341ba71aa55df92f5de99da11396ce50578700.
■