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_137f848bdb78f472068da9f3e5698255d8403888e1b30f209fd7da0af03ad2f1 with
9f253...
The subproof is completed by applying L0.