Let x0 of type ι be given.
Apply H0 with
struct_p x0.
Assume H2:
unpack_p_o x0 (λ x1 . λ x2 : ι → ο . ∃ x3 . and (x3 ∈ x1) (x2 x3)).
The subproof is completed by applying H1.
Apply unknownprop_8e7946e14374f929755e19a1c44c77701625a3b4110f6a053a055efef5fccc73 with
PtdPred.
The subproof is completed by applying L0.