Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Let x1 of type ιο be given.
Assume H0: 3a6d0.. (407b5.. x0) (407b5.. x1).
Apply unknownprop_496f21822a3fb678f9d36a054a8a41e367bd46550d4cc9d277917362980b9e62 with 407b5.. x0, 407b5.. x1, λ x2 : (ι → ο) → ο . x2 = 407b5.. x0d97e3.. x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ιο be given.
Assume H1: d97e3.. x2 x1.
Assume H2: 407b5.. x2 = 407b5.. x0.
Apply unknownprop_f6212d6ba4366f14f16f0857e6566c26f7bd27125deb5e4c2748921fd5fa9530 with x2, x0, λ x3 x4 : ι → ο . d97e3.. x3 x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x2 of type ((ιο) → ο) → ((ιο) → ο) → ο be given.
Assume H1: x2 (407b5.. x0) (407b5.. x0).
The subproof is completed by applying H1.