| λ x0 . and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . and (and (and (and (and (and (and (and (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x2 (x2 x6 x7) x8 = x2 x6 (x2 x7 x8)) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ x2 x6 x7 = x2 x7 x6)) (∀ x6 . x6 ∈ x1 ⟶ x2 x6 x4 = x6)) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 (x3 x6 x7) x8 = x3 x6 (x3 x7 x8))) (∀ x6 . x6 ∈ x1 ⟶ and (x3 x6 x5 = x6) (x3 x5 x6 = x6))) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 x6 (x2 x7 x8) = x2 (x3 x6 x7) (x3 x6 x8))) (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 (x2 x6 x7) x8 = x2 (x3 x6 x8) (x3 x7 x8))) (∀ x6 . x6 ∈ x1 ⟶ x3 x6 x4 = x4)) (∀ x6 . x6 ∈ x1 ⟶ x3 x4 x6 = x4))) |
|