| λ x0 x1 x2 . unpack_b_b_e_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 x7 . unpack_b_b_e_e_o x1 (λ x8 . λ x9 x10 : ι → ι → ι . λ x11 x12 . and (and (and (and (x2 ∈ setexp x8 x3) (∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ap x2 (x4 x13 x14) = x9 (ap x2 x13) (ap x2 x14))) (∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ap x2 (x5 x13 x14) = x10 (ap x2 x13) (ap x2 x14))) (ap x2 x6 = x11)) (ap x2 x7 = x12))) |
|
|
|
|
|
|
|
|
|
|