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