Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Assume H0:
∃ x2 . and (x2 ∈ x0) (x1 x2).
Apply andI with
struct_p (pack_p x0 x1),
unpack_p_o (pack_p x0 x1) (λ x2 . λ x3 : ι → ο . ∃ x4 . and (x4 ∈ x2) (x3 x4)) leaving 2 subgoals.
The subproof is completed by applying pack_struct_p_I with x0, x1.
Apply unpack_p_o_eq with
λ x2 . λ x3 : ι → ο . ∃ x4 . and (x4 ∈ x2) (x3 x4),
x0,
x1,
λ x2 x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b2592fa24ced3d84e007e876699c34520860460028b2dc9144c228a16f98ce34 with x0, x1.
The subproof is completed by applying H0.