Let x0 of type (ι → ο) → ο be given.
Let x1 of type ο be given.
Apply H0 with
x0.
Let x2 of type (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο be given.
The subproof is completed by applying H1.
Let x1 of type (ι → ο) → ο be given.
Let x2 of type (ι → ο) → ο be given.
Apply unknownprop_0baf4c86bc102cc7ef5b5a6fba0fc5f1dad77a50acb8dbafd746ed7c6f61a4d8 with
x2,
x0,
λ x3 x4 : (ι → ο) → ο . x1 = x4 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_0baf4c86bc102cc7ef5b5a6fba0fc5f1dad77a50acb8dbafd746ed7c6f61a4d8 with
x1,
x0.
The subproof is completed by applying H1.
Apply Descr_Vo2_prop with
λ x1 : (ι → ο) → ο . a4b00.. x1 = a4b00.. x0 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply unknownprop_0baf4c86bc102cc7ef5b5a6fba0fc5f1dad77a50acb8dbafd746ed7c6f61a4d8 with
d94e6.. (a4b00.. x0),
x0.
The subproof is completed by applying L2.