Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply tuple_3_eta with
x0,
x1,
x2,
λ x3 x4 . x3 = 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)).
Apply set_ext with
lam 3 (ap (lam 3 (λ x3 . If_i (x3 = 0) x0 (If_i (x3 = 1) x1 x2)))),
4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)) leaving 2 subgoals.
Let x3 of type ι be given.
Assume H0:
x3 ∈ lam 3 (λ x4 . ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) x4).
Apply unknownprop_7e890e3c212f35a253b09f8bdf3ce512e10f8816e882a3da817fe1bc10582407 with
3,
λ x4 . ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) x4,
x3,
x3 ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Assume H1: x4 ∈ 3.
Let x5 of type ι be given.
Assume H2:
x5 ∈ ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) x4.
Assume H3:
x3 = lam 2 (λ x6 . If_i (x6 = 0) x4 x5).
Apply H3 with
λ x6 x7 . x7 ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)).
Apply cases_3 with
x4,
λ x6 . x5 ∈ ap (lam 3 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 x2))) x6 ⟶ lam 2 (λ x7 . If_i (x7 = 0) x6 x5) ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)) leaving 5 subgoals.
The subproof is completed by applying H1.
Apply tuple_3_0_eq with
x0,
x1,
x2,
λ x6 x7 . x5 ∈ x7 ⟶ lam 2 (λ x8 . If_i (x8 = 0) 0 x5) ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)).
Assume H4: x5 ∈ x0.
Apply unknownprop_f7f95af90cf38c6ac02d3898eb74c239c35f5e3ce91d1753f7cf74b0093030b8 with
x0,
4ec03.. x1 (4ec03.. x2 0),
0,
x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with
x0,
4ec03.. x1 (4ec03.. x2 0),
λ x6 x7 . x5 ∈ x7.
The subproof is completed by applying H4.
Apply tuple_3_1_eq with
x0,
x1,
x2,
λ x6 x7 . x5 ∈ x7 ⟶ lam 2 (λ x8 . If_i (x8 = 0) 1 x5) ∈ 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)).
Assume H4: x5 ∈ x1.
Apply unknownprop_f7f95af90cf38c6ac02d3898eb74c239c35f5e3ce91d1753f7cf74b0093030b8 with
x0,
4ec03.. x1 (4ec03.. x2 0),
1,
x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_5a07df7ee1e82c544809d0445743f3daa0dcce88f316504384ce6ecc51761fc3.
Apply unknownprop_4270b0e920f6ab49c5577490ca19e4c5c6282a2ea155f48817cbf066c86da489 with
x0,
4ec03.. x1 (4ec03.. x2 0),
0,
λ x6 x7 . x5 ∈ x7 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with
x1,
4ec03.. x2 0,
λ x6 x7 . x5 ∈ x7.
The subproof is completed by applying H4.
Apply tuple_3_2_eq with
x0,
x1,
x2,
λ x6 x7 . ... ⟶ lam 2 ... ∈ ....