| λ x0 x1 . unpack_b_i x1 (λ x2 . λ x3 : ι → ι → ι . {x4 ∈ omega|∀ x5 : ο . (∀ x6 . and (x6 ∈ setexp x2 (ordsucc x4)) (∀ x7 . x7 ∈ ordsucc x4 ⟶ ∀ x8 . x8 ∈ ordsucc x4 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ ∀ x9 . x9 ∈ ap x0 0 ⟶ ∀ x10 . x10 ∈ ap x0 0 ⟶ x3 (ap x6 x7) x9 = x3 (ap x6 x8) x10 ⟶ ∀ x11 : ο . x11) ⟶ x5) ⟶ x5}) |
|