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