| ∀ x0 . ∀ x1 : ι → ι → ο . unpack_r_o (pack_r x0 x1) (λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) = and (∀ x3 . x3 ∈ x0 ⟶ not (x1 x3 x3)) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 ⟶ x1 x4 x3) |
|