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