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_59e3f3dce052073bbe68f49c7125d7f995693bb360ddfee771c0265ad2f4452d with
PtdPred.
The subproof is completed by applying L0.