Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (ιο) → ο be given.
Let x1 of type (ιο) → ο be given.
Assume H0: a4b00.. x0 = a4b00.. x1.
Apply functional extensionality with x0, x1.
Let x2 of type ιο be given.
Apply prop_ext_2 with x0 x2, x1 x2 leaving 2 subgoals.
Assume H1: x0 x2.
Claim L2: a4b00.. x1 (407b5.. x2)
Apply H0 with λ x3 x4 : ((ι → ο) → ο) → ο . x3 (407b5.. x2).
Let x3 of type ο be given.
Assume H2: ∀ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x0 x4)x3.
Apply H2 with x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with 407b5.. x2 = 407b5.. x2, x0 x2 leaving 2 subgoals.
Let x4 of type ((ιο) → ο) → ((ιο) → ο) → ο be given.
Assume H3: x4 (407b5.. x2) (407b5.. x2).
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply L2 with x1 x2.
Let x3 of type ιο be given.
Assume H3: (λ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x1 x4)) x3.
Apply andE with 407b5.. x2 = 407b5.. x3, x1 x3, x1 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4: 407b5.. x2 = 407b5.. x3.
Assume H5: x1 x3.
Apply unknownprop_f6212d6ba4366f14f16f0857e6566c26f7bd27125deb5e4c2748921fd5fa9530 with x2, x3, λ x4 x5 : ι → ο . x1 x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H1: x1 x2.
Claim L2: a4b00.. x0 (407b5.. x2)
Apply H0 with λ x3 x4 : ((ι → ο) → ο) → ο . x4 (407b5.. x2).
Let x3 of type ο be given.
Assume H2: ∀ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x1 x4)x3.
Apply H2 with x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with 407b5.. x2 = 407b5.. x2, x1 x2 leaving 2 subgoals.
Let x4 of type ((ιο) → ο) → ((ιο) → ο) → ο be given.
Assume H3: x4 (407b5.. x2) (407b5.. x2).
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Apply L2 with x0 x2.
Let x3 of type ιο be given.
Assume H3: (λ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x0 x4)) x3.
Apply andE with 407b5.. x2 = 407b5.. x3, x0 x3, x0 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4: 407b5.. x2 = 407b5.. x3.
Assume H5: x0 x3.
Apply unknownprop_f6212d6ba4366f14f16f0857e6566c26f7bd27125deb5e4c2748921fd5fa9530 with x2, x3, λ x4 x5 : ι → ο . x0 x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.