Let x0 of type (ι → ι → ο) → ο be given.
Assume H0: ∃ x1 : ι → ι → ο . x0 x1.
Assume H1: ∀ x1 x2 : ι → ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2.
Apply H0 with
x0 (Descr_iio x0).
Let x1 of type ι → ι → ο be given.
Assume H2: x0 x1.
Apply functional extensionality with
x1,
Descr_iio x0.
Let x2 of type ι be given.
Apply functional extensionality with
x1 x2,
Descr_iio x0 x2.
Let x3 of type ι be given.
Apply prop_ext_2 with
x1 x2 x3,
Descr_iio x0 x2 x3 leaving 2 subgoals.
Assume H3: x1 x2 x3.
Let x4 of type ι → ι → ο be given.
Assume H4: x0 x4.
Apply H1 with
x1,
x4,
λ x5 x6 : ι → ι → ο . x5 x2 x3 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Apply H3 with
x1.
The subproof is completed by applying H2.
Apply L3 with
λ x2 x3 : ι → ι → ο . x0 x2.
The subproof is completed by applying H2.