Let x0 of type ι → ο be given.
Let x1 of type ι → ο be given.
Apply unknownprop_496f21822a3fb678f9d36a054a8a41e367bd46550d4cc9d277917362980b9e62 with
407b5.. x0,
407b5.. x1,
λ x2 : (ι → ο) → ο . x2 = 407b5.. x0 ⟶ d97e3.. x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι → ο be given.
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.
The subproof is completed by applying H1.