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