Let x0 of type ι be given.
Apply H0 with
struct_u x0.
Assume H2:
unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3).
The subproof is completed by applying H1.
Apply unknownprop_6809a8ae9ac2e08c74bb19682836f899f1647bfb19e1beda778b023f38a68650 with
9f253...
The subproof is completed by applying L0.