Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
λ x2 . struct_p (f5637.. x2 x1).
Let x2 of type ι be given.
Let x3 of type ι → ο be given.
Apply H1 with
λ x4 . struct_p (f5637.. (pack_p x2 x3) x4).
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Apply unknownprop_8a66e4bdb214ee413447ac05cf120a4276b1afb59a2fc210ec5bfee37471a43f with
x2,
x3,
x4,
x5,
λ x6 x7 . struct_p x7.
The subproof is completed by applying pack_struct_p_I with
setexp x4 x2,
λ x6 . ∀ x7 . x7 ∈ x2 ⟶ x3 x7 ⟶ x5 (ap x6 x7).