| ∀ x0 . 6e587.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . ∀ x4 . x4 ∈ x2 ⟶ (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x5 x6 ∈ x2) ⟶ (∀ x5 . x5 ∈ x2 ⟶ and (x3 x5 x4 = x5) (x3 x4 x5 = x5)) ⟶ (∀ x5 . x5 ∈ x2 ⟶ bij x2 x2 (x3 x5)) ⟶ (∀ x5 . x5 ∈ x2 ⟶ bij x2 x2 (λ x6 . x3 x6 x5)) ⟶ x1 (pack_b x2 x3)) ⟶ x1 x0 |
|