Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (ι → ι → ι) → ι → ι → ι be given.
Assume H0: ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1).
Apply unknownprop_6891c2c4cbe5dbf32677e09d76954ef64727a2786342d5026c3517fb0288e38a with x0 ChurchBoolTru, x0 ChurchBoolFal, λ x1 x2 : ο . x2 = ∀ x3 : ι → ι → ι . fb516.. x3 ⟶ 6fb7f.. (x0 x3) leaving 3 subgoals.
Apply H0 with ChurchBoolTru.
The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.
Apply H0 with ChurchBoolFal.
The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.
Apply prop_ext_2 with and (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)), ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ 6fb7f.. (x0 x1) leaving 2 subgoals.
Assume H1: and (6fb7f.. (x0 ChurchBoolTru)) (6fb7f.. (x0 ChurchBoolFal)).
Apply H1 with ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ 6fb7f.. (x0 x1).
Assume H2: 6fb7f.. (x0 ChurchBoolTru).
Assume H3: 6fb7f.. (x0 ChurchBoolFal).
Let x1 of type ι → ι → ι be given.
Assume H4: fb516.. x1.
Apply H4 with 6fb7f.. (x0 x1) leaving 2 subgoals.
Assume H5: x1 = ChurchBoolTru.
Apply H5 with λ x2 x3 : ι → ι → ι . 6fb7f.. (x0 x3).
The subproof is completed by applying H2.
Assume H5: x1 = ChurchBoolFal.
Apply H5 with λ x2 x3 : ι → ι → ι . 6fb7f.. (x0 x3).
The subproof is completed by applying H3.
Assume H1: ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ 6fb7f.. (x0 x1).
Apply andI with 6fb7f.. (x0 ChurchBoolTru), 6fb7f.. (x0 ChurchBoolFal) leaving 2 subgoals.
Apply H1 with ChurchBoolTru.
The subproof is completed by applying unknownprop_4b2c4a0487c2b1a228c5d07bbf352ffca25633bec988b0f94ee850e02347e107.
Apply H1 with ChurchBoolFal.
The subproof is completed by applying unknownprop_5066d1b2b30c335c067f01ac13f147e53d00378a90e5b6ab1432446a8181f6dd.
■