Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
e5b72.. (0fc90.. x0 (λ x4 . prim3 (x1 x4))),
λ x4 . ∀ x5 . prim1 x5 x0 ⟶ prim1 (f482f.. x4 x5) (x1 x5),
x2,
x3.
The subproof is completed by applying H0.