Let x0 of type ((ι → ο) → ο) → ο be given.
Let x1 of type ((ι → ο) → ο) → ο be given.
Apply unknownprop_c6664f1abdc99ace6d817e614743060b949620a298baacd98ca5336d448b8e3b with
a327b.. x0,
a327b.. x1,
λ x2 : (((ι → ο) → ο) → ο) → ο . x2 = a327b.. x0 ⟶ e6217.. x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ((ι → ο) → ο) → ο be given.
Apply unknownprop_fb936e779a336113a4fb7f3c7b779c1e8f8958132dfedde97188f6d659f336c8 with
x2,
x0,
λ x3 x4 : ((ι → ο) → ο) → ο . e6217.. 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.