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_fb936e779a336113a4fb7f3c7b779c1e8f8958132dfedde97188f6d659f336c8 with
x2,
x0,
λ x3 x4 : ((ι → ο) → ο) → ο . x1 = x4 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_fb936e779a336113a4fb7f3c7b779c1e8f8958132dfedde97188f6d659f336c8 with
x1,
x0.
The subproof is completed by applying H1.
Apply Descr_Vo3_prop with
λ x1 : ((ι → ο) → ο) → ο . a327b.. x1 = a327b.. x0 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
Apply unknownprop_fb936e779a336113a4fb7f3c7b779c1e8f8958132dfedde97188f6d659f336c8 with
dba53.. (a327b.. x0),
x0.
The subproof is completed by applying L2.