Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ι(((ιο) → ο) → ο) → ο) → (((ιο) → ο) → ο) → ο be given.
Assume H0: ∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . In x4 x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3.
Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with λ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x1 x277406.. x0 x1 x3x2 = x3.
Let x1 of type ι be given.
Assume H1: ∀ x2 . In x2 x1∀ x3 x4 : (((ι → ο) → ο) → ο) → ο . 77406.. x0 x2 x377406.. x0 x2 x4x3 = x4.
Let x2 of type (((ιο) → ο) → ο) → ο be given.
Let x3 of type (((ιο) → ο) → ο) → ο be given.
Assume H2: 77406.. x0 x1 x2.
Assume H3: 77406.. x0 x1 x3.
Claim L4: ∃ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . In x5 x177406.. x0 x5 (x4 x5)) (x2 = x0 x1 x4)
Apply unknownprop_48b464cf39ccff01457820decb42248ce18524a5c9844b352085ede155a989e6 with x0, x1, x2.
The subproof is completed by applying H2.
Claim L5: ∃ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . In x5 x177406.. x0 x5 (x4 x5)) (x3 = x0 x1 x4)
Apply unknownprop_48b464cf39ccff01457820decb42248ce18524a5c9844b352085ede155a989e6 with x0, x1, x3.
The subproof is completed by applying H3.
Apply L4 with x2 = x3.
Let x4 of type ι(((ιο) → ο) → ο) → ο be given.
Assume H6: (λ x5 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x6 . In x6 x177406.. x0 x6 (x5 x6)) (x2 = x0 x1 x5)) x4.
Apply andE with ∀ x5 . In x5 x177406.. x0 x5 (x4 x5), x2 = x0 x1 x4, x2 = x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: ∀ x5 . In x5 x177406.. x0 x5 (x4 x5).
Assume H8: x2 = x0 x1 x4.
Apply L5 with x2 = x3.
Let x5 of type ι(((ιο) → ο) → ο) → ο be given.
Assume H9: (λ x6 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x7 . In x7 x177406.. x0 x7 (x6 x7)) (x3 = x0 x1 x6)) x5.
Apply andE with ∀ x6 . In x6 x177406.. x0 x6 (x5 x6), x3 = x0 x1 x5, x2 = x3 leaving 2 subgoals.
The subproof is completed by applying H9.
Assume H10: ∀ x6 . In x6 x177406.. x0 x6 (x5 x6).
Assume H11: x3 = x0 x1 x5.
Apply H8 with λ x6 x7 : (((ι → ο) → ο) → ο) → ο . x7 = x3.
Apply H11 with λ x6 x7 : (((ι → ο) → ο) → ο) → ο . x0 x1 x4 = x7.
Apply H0 with x1, x4, x5.
Let x6 of type ι be given.
Assume H12: In x6 x1.
Apply H1 with x6, x4 x6, x5 x6 leaving 3 subgoals.
The subproof is completed by applying H12.
Apply H7 with x6.
The subproof is completed by applying H12.
Apply H10 with x6.
The subproof is completed by applying H12.