Let x0 of type ο be given.
Apply H0 with
pack_p 1 (λ x1 . True).
Let x1 of type ο be given.
Apply H1 with
λ x2 . lam (ap x2 0) (λ x3 . 0).
Apply andI with
struct_p (pack_p 1 (λ x2 . True)),
∀ x2 . struct_p x2 ⟶ and (UnaryPredHom x2 (pack_p 1 (λ x3 . True)) (lam (ap x2 0) (λ x3 . 0))) (∀ x3 . UnaryPredHom x2 (pack_p 1 (λ x4 . True)) x3 ⟶ x3 = lam (ap x2 0) (λ x4 . 0)) leaving 2 subgoals.
The subproof is completed by applying pack_struct_p_I with
1,
λ x2 . True.
Let x2 of type ι be given.
Apply H2 with
λ x3 . and (UnaryPredHom x3 (pack_p 1 (λ x4 . True)) (lam (ap x3 0) (λ x4 . 0))) (∀ x4 . UnaryPredHom x3 (pack_p 1 (λ x5 . True)) x4 ⟶ x4 = lam (ap x3 0) (λ x5 . 0)).
Let x3 of type ι be given.
Let x4 of type ι → ο be given.
Apply andI with
UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x5 . True)) (lam (ap (pack_p x3 x4) 0) (λ x5 . 0)),
∀ x5 . UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x6 . True)) x5 ⟶ x5 = lam (ap (pack_p x3 x4) 0) (λ x6 . 0) leaving 2 subgoals.
Apply pack_p_0_eq2 with
x3,
x4,
λ x5 x6 . UnaryPredHom (pack_p x3 x4) (pack_p 1 (λ x7 . True)) (lam x5 (λ x7 . 0)).
Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with
x3,
1,
x4,
λ x5 . True,
lam x3 (λ x5 . 0),
λ x5 x6 : ο . x6.
Apply andI with
lam x3 (λ x5 . 0) ∈ setexp 1 x3,
∀ x5 . x5 ∈ x3 ⟶ x4 x5 ⟶ (λ x6 . True) (ap (lam x3 (λ x6 . 0)) x5) leaving 2 subgoals.
Apply lam_Pi with
x3,
λ x5 . 1,
λ x5 . 0.
Let x5 of type ι be given.
Assume H3: x5 ∈ x3.
The subproof is completed by applying In_0_1.
Let x5 of type ι be given.
Assume H3: x5 ∈ x3.
Assume H4: x4 x5.
The subproof is completed by applying TrueI.
Let x5 of type ι be given.
Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with
x3,
1,
x4,
λ x6 . True,
x5,
λ x6 x7 : ο . x7 ⟶ x5 = lam (ap (pack_p x3 x4) 0) (λ x8 . 0).
Assume H3:
and (x5 ∈ setexp 1 x3) (∀ x6 . x6 ∈ x3 ⟶ x4 x6 ⟶ True).
Apply H3 with
x5 = lam (ap (pack_p x3 x4) 0) (λ x6 . 0).
Assume H4:
x5 ∈ Pi x3 (λ x6 . 1).
Assume H5:
∀ x6 . ... ∈ ... ⟶ x4 x6 ⟶ True.