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