| ∀ x0 . ∀ x1 : ι → ι → ι . unpack_b_o (pack_b x0 x1) (λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x7 . x7 ∈ x3 ⟶ and (x4 x7 x5 = x7) (x4 x5 x7 = x7))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (x4 x5))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) = and (and (∃ x3 . and (x3 ∈ x0) (∀ x5 . x5 ∈ x0 ⟶ and (x1 x5 x3 = x5) (x1 x3 x5 = x5))) (∀ x3 . x3 ∈ x0 ⟶ bij x0 x0 (x1 x3))) (∀ x3 . x3 ∈ x0 ⟶ bij x0 x0 (λ x4 . x1 x4 x3)) |
|