Let x0 of type ι be given.
Assume H2: 0 ∈ x0.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ι → ι be given.
Assume H4: ∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0.
Apply unknownprop_9b1382fd828c310f237a34618b8aad95180eb391959d046ef1956fa7f3460a59 with
x1,
x2,
λ x3 . x3 ∈ x0.
Let x3 of type ι be given.
Assume H5: x3 ∈ x1.
Let x4 of type ι be given.
Assume H7:
∀ x5 . x5 ∈ x2 x3 ⟶ 59caa.. x1 x2 (ap x4 x5).
Assume H8:
∀ x5 . x5 ∈ x2 x3 ⟶ ap x4 x5 ∈ x0.
Apply unknownprop_907e5d06a6b2bc734b7a7ddcb472ccf64af6b48c6f2955dc95c2cd40b0a7420f with
x0,
2,
lam 2 (λ x5 . If_i (x5 = 0) x3 x4) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_79d5b41f0dcf32b9d9037781ca155b625d84c7a59be9fd2f760cb594e4cdaa69 with
x0,
2 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying nat_2.
The subproof is completed by applying tuple_p_2_tuple with x3, x4.
Let x5 of type ι be given.
Assume H9: x5 ∈ 2.
Apply cases_2 with
x5,
λ x6 . ap (lam 2 (λ x7 . If_i (x7 = 0) x3 x4)) x6 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H9.
Apply tuple_2_0_eq with
x3,
x4,
λ x6 x7 . x7 ∈ x0.
Apply H0 with
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Apply tuple_2_1_eq with
x3,
x4,
λ x6 x7 . x7 ∈ x0.
Apply unknownprop_907e5d06a6b2bc734b7a7ddcb472ccf64af6b48c6f2955dc95c2cd40b0a7420f with
x0,
x2 x3,
x4 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H4 with
x3.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H8.