Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ι → ι be given.
Let x3 of type ι be given.
Assume H0: x3 ∈ x0.
Let x4 of type ι be given.
Assume H2:
∀ x5 . x5 ∈ x1 x3 ⟶ ap x4 x5 ∈ c8f46.. x0 (λ x6 . x1 x6).
Claim L3:
lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ c8f46.. x0 (λ x5 . x1 x5)Apply unknownprop_f9f7f36b256ee5022d975788009d4c406b63c7d7fc85dc77b1112d548d8ed23a with
x0,
λ x5 . x1 x5,
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply Eps_i_ex with
c40a3.. x0 x1 x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)).
Apply unknownprop_e4f6484ffbc2d471a495e328d25286ba48e9116ed79c963b7f06599e26869546 with
x0,
x1,
x2,
lam 2 (λ x5 . If_i (x5 = 0) x3 x4).
The subproof is completed by applying L3.
Apply unknownprop_412f171b3ca442889854b1b6db1f4b4c229650705be86611715b49239feb0217 with
x0,
x1,
x2,
x3,
x4,
λ x5 . e2778.. x0 x1 x2 (ap x4 x5) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x5 of type ι be given.
Assume H5: x5 ∈ x1 x3.
Apply Eps_i_ex with
c40a3.. x0 x1 x2 (ap x4 x5).
Apply unknownprop_e4f6484ffbc2d471a495e328d25286ba48e9116ed79c963b7f06599e26869546 with
x0,
x1,
x2,
ap x4 x5.
Apply H2 with
x5.
The subproof is completed by applying H5.
Apply unknownprop_7a71f3a0731394e6a0eaedc69e45f2fcf8a1da06bc07aeb04d21038798d39d0f with
x0,
x1,
x2,
lam 2 (λ x5 . If_i (x5 = 0) x3 x4),
e2778.. x0 x1 x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)),
lam 2 (λ x5 . If_i (x5 = 0) x3 x4),
x2 x3 x4 (lam (x1 x3) (λ x5 . e2778.. x0 x1 x2 (ap x4 x5))) leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Assume H6:
x5 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)).
The subproof is completed by applying H6.