Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply tuple_4_eta with
x0,
x1,
x2,
x3,
λ x4 x5 . x4 = 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))).
Apply set_ext with
lam 4 (ap (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3))))),
4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))) leaving 2 subgoals.
Let x4 of type ι be given.
Assume H0:
x4 ∈ lam 4 (λ x5 . ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 x3)))) x5).
Apply unknownprop_7e890e3c212f35a253b09f8bdf3ce512e10f8816e882a3da817fe1bc10582407 with
4,
λ x5 . ap (lam 4 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 x3)))) x5,
x4,
x4 ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x5 of type ι be given.
Assume H1: x5 ∈ 4.
Let x6 of type ι be given.
Assume H2:
x6 ∈ ap (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 x3)))) x5.
Assume H3:
x4 = lam 2 (λ x7 . If_i (x7 = 0) x5 x6).
Apply H3 with
λ x7 x8 . x8 ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))).
Apply cases_4 with
x5,
λ x7 . x6 ∈ ap (lam 4 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 (If_i (x8 = 2) x2 x3)))) x7 ⟶ lam 2 (λ x8 . If_i (x8 = 0) x7 x6) ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))) leaving 6 subgoals.
The subproof is completed by applying H1.
Apply tuple_4_0_eq with
x0,
x1,
x2,
x3,
λ x7 x8 . x6 ∈ x8 ⟶ lam 2 (λ x9 . If_i (x9 = 0) 0 x6) ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))).
Assume H4: x6 ∈ x0.
Apply unknownprop_f7f95af90cf38c6ac02d3898eb74c239c35f5e3ce91d1753f7cf74b0093030b8 with
x0,
4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0)),
0,
x6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with
x0,
4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0)),
λ x7 x8 . x6 ∈ x8.
The subproof is completed by applying H4.
Apply tuple_4_1_eq with
x0,
x1,
x2,
x3,
λ x7 x8 . ... ⟶ lam 2 (λ x9 . If_i (x9 = 0) 1 x6) ∈ 4ec03.. ... ....