Let x0 of type ι be given.
Let x1 of type ι be given.
Apply tuple_2_eta with
x0,
x1,
λ x2 x3 . x2 = 4ec03.. x0 (4ec03.. x1 0).
Apply set_ext with
lam 2 (ap (lam 2 (λ x2 . If_i (x2 = 0) x0 x1))),
4ec03.. x0 (4ec03.. x1 0) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H0:
x2 ∈ lam 2 (λ x3 . ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) x3).
Apply unknownprop_7e890e3c212f35a253b09f8bdf3ce512e10f8816e882a3da817fe1bc10582407 with
2,
λ x3 . ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) x3,
x2,
x2 ∈ 4ec03.. x0 (4ec03.. x1 0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1: x3 ∈ 2.
Let x4 of type ι be given.
Assume H2:
x4 ∈ ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x3.
Assume H3:
x2 = lam 2 (λ x5 . If_i (x5 = 0) x3 x4).
Apply H3 with
λ x5 x6 . x6 ∈ 4ec03.. x0 (4ec03.. x1 0).
Apply cases_2 with
x3,
λ x5 . x4 ∈ ap (lam 2 (λ x6 . If_i (x6 = 0) x0 x1)) x5 ⟶ lam 2 (λ x6 . If_i (x6 = 0) x5 x4) ∈ 4ec03.. x0 (4ec03.. x1 0) leaving 4 subgoals.
The subproof is completed by applying H1.
Apply tuple_2_0_eq with
x0,
x1,
λ x5 x6 . x4 ∈ x6 ⟶ lam 2 (λ x7 . If_i (x7 = 0) 0 x4) ∈ 4ec03.. x0 (4ec03.. x1 0).
Assume H4: x4 ∈ x0.
Apply unknownprop_f7f95af90cf38c6ac02d3898eb74c239c35f5e3ce91d1753f7cf74b0093030b8 with
x0,
4ec03.. x1 0,
0,
x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with
x0,
4ec03.. x1 0,
λ x5 x6 . x4 ∈ x6.
The subproof is completed by applying H4.
Apply tuple_2_1_eq with
x0,
x1,
λ x5 x6 . x4 ∈ x6 ⟶ lam 2 (λ x7 . If_i (x7 = 0) 1 x4) ∈ 4ec03.. x0 (4ec03.. x1 0).
Assume H4: x4 ∈ x1.
Apply unknownprop_f7f95af90cf38c6ac02d3898eb74c239c35f5e3ce91d1753f7cf74b0093030b8 with
x0,
4ec03.. x1 0,
1,
x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_5a07df7ee1e82c544809d0445743f3daa0dcce88f316504384ce6ecc51761fc3.
Apply unknownprop_4270b0e920f6ab49c5577490ca19e4c5c6282a2ea155f48817cbf066c86da489 with
x0,
4ec03.. x1 0,
0,
λ x5 x6 . x4 ∈ x6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87d981ec36961a0324ea5d0962fa0689e652a1a367082910c100751340d2d034.
Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with
x1,
0,
λ x5 x6 . x4 ∈ x6.
The subproof is completed by applying H4.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Apply unknownprop_a3a28db1ee360c88e08a9998e3eec43955f297f7894a630aecacc7c87146ecf9 with
x0,
4ec03.. x1 0,
x2,
x2 ∈ lam 2 (λ x3 . ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Apply unknownprop_88b2ea790bcab2ae0ee80f7c15366cb971f56af74a5ab2ee5a48de291b7dc4b5 with
x3,
λ x4 . ∀ x5 . ... ⟶ x2 = lam 2 ... ⟶ x2 ∈ lam 2 (λ x6 . ap (lam 2 (λ x7 . If_i (x7 = 0) x0 x1)) x6) leaving 3 subgoals.