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_2576d2815b46016e5e13a9989b4e9789629d83c56ed1c92a4cda0de077a20752 with
1,
λ x0 . True.
Let x0 of type ο be given.
Assume H1:
∀ x1 . and (x1 ∈ 1) ((λ x2 . True) x1) ⟶ x0.
Apply H1 with
0.
Apply andI with
0 ∈ 1,
(λ x1 . True) 0 leaving 2 subgoals.
The subproof is completed by applying In_0_1.
The subproof is completed by applying TrueI.
Apply unknownprop_eaa5ecc21d9729bc79b0e5cf0bed2c98f0fc7f7f801ce2eeca3ce9b80a339bb2 with
PtdPred leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.