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