Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Claim L0:
∀ x2 x3 x4 . ... ⟶ (λ x5 x6 . and (x1 x5) (x5 = x6)) x2 x4 ⟶ x3 = x4
Apply unknownprop_aaea0f1d3f5e853f0d3287d822ec5f356e024921388ea00672dad551690ba08f with
x0,
λ x2 x3 . and (x1 x2) (x2 = x3).
The subproof is completed by applying L0.
Apply L1 with
∃ x2 . ∀ x3 . iff (prim1 x3 x2) (and (prim1 x3 x0) (x1 x3)).
Let x2 of type ι be given.
Assume H2:
(λ x3 . ∀ x4 . iff (prim1 x4 x3) (∃ x5 . and (prim1 x5 x0) (and (x1 x5) (x5 = x4)))) x2.
Let x3 of type ο be given.
Apply H3 with
x2.
Let x4 of type ι be given.
Apply H2 with
x4,
iff (prim1 x4 x2) (and (prim1 x4 x0) (x1 x4)).
Apply iffI with
prim1 x4 x2,
and (prim1 x4 x0) (x1 x4) leaving 2 subgoals.
Apply H4 with
and (prim1 x4 x0) (x1 x4) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H7:
(λ x6 . and (prim1 x6 x0) (and (x1 x6) (x6 = x4))) x5.
Apply H7 with
and (prim1 x4 x0) (x1 x4).
Assume H9:
and (x1 x5) (x5 = x4).
Apply H9 with
and (prim1 x4 x0) (x1 x4).
Assume H10: x1 x5.
Assume H11: x5 = x4.
Apply andI with
prim1 x4 x0,
x1 x4 leaving 2 subgoals.
Apply H11 with
λ x6 x7 . prim1 x6 x0.
The subproof is completed by applying H8.
Apply H11 with
λ x6 x7 . x1 x6.
The subproof is completed by applying H10.
Apply H6 with
prim1 x4 x2.
Assume H8: x1 x4.
Apply H5.
Let x5 of type ο be given.
Assume H9:
∀ x6 . and (prim1 x6 x0) (and (x1 x6) (x6 = x4)) ⟶ x5.
Apply H9 with
x4.
Apply andI with
prim1 x4 x0,
and (x1 x4) (x4 = x4) leaving 2 subgoals.
The subproof is completed by applying H7.
Apply andI with
x1 x4,
x4 = x4 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x6 of type ι → ι → ο be given.
Assume H10: x6 x4 x4.
The subproof is completed by applying H10.