| ∀ x0 : ο . ((∀ x1 : ι → ο . (∀ x2 x3 . x1 x3) ⟶ ∀ x2 x3 . x1 x3) ⟶ (∀ x1 : ι → ι → ο . ∀ x2 x3 . wceq (cv x2) (cv x3) ⟶ (∀ x4 . x1 x2 x4) ⟶ ∀ x4 . wceq (cv x4) (cv x3) ⟶ x1 x4 x3) ⟶ (∀ x1 : ι → ο . ∀ x2 . wceq (cv x2) (cv x2) ⟶ (∀ x3 . x1 x3) ⟶ ∀ x3 . wceq (cv x3) (cv x3) ⟶ x1 x3) ⟶ (∀ x1 x2 x3 . wn (wceq (cv x3) (cv x1)) ⟶ wceq (cv x1) (cv x2) ⟶ ∀ x4 . wceq (cv x1) (cv x2)) ⟶ (∀ x1 x2 . wn (wceq (cv x2) (cv x2)) ⟶ wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x1)) ⟶ (∀ x1 : ι → ο . wb (weu x1) (wex (λ x2 . ∀ x3 . wb (x1 x3) (wceq (cv x3) (cv x2))))) ⟶ (∀ x1 : ι → ο . wb (wmo x1) (wex x1 ⟶ weu x1)) ⟶ (∀ x1 x2 . (∀ x3 . wb (wcel (cv x3) (cv x1)) (wcel (cv x3) (cv x2))) ⟶ wceq (cv x1) (cv x2)) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wcel (cv x2) (cab x1)) (wsb x1 x2)) ⟶ (∀ x1 : ι → ο . ∀ x2 . wb (wcel (cv x2) (cab x1)) (wsb x1 x2)) ⟶ (∀ x1 x2 : ι → ι → ι → ο . (∀ x3 x4 . (∀ x5 . wb (wcel (cv x5) (cv x3)) (wcel (cv x5) (cv x4))) ⟶ wceq (cv x3) (cv x4)) ⟶ ∀ x3 x4 . wb (wceq (x1 x3 x4) (x2 x3 x4)) (∀ x5 . wb (wcel (cv x5) (x1 x3 x4)) (wcel (cv x5) (x2 x3 x4)))) ⟶ (∀ x1 x2 : ι → ο . wb (wcel x1 x2) (wex (λ x3 . wa (wceq (cv x3) x1) (wcel (cv x3) x2)))) ⟶ (∀ x1 : ι → ι → ο . wb (wnfc x1) (∀ x2 . wnf (λ x3 . wcel (cv x2) (x1 x3)))) ⟶ (∀ x1 x2 : ι → ο . wb (wne x1 x2) (wn (wceq x1 x2))) ⟶ (∀ x1 x2 : ι → ο . wb (wnel x1 x2) (wn (wcel x1 x2))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wral x1 x2) (∀ x3 . wcel (cv x3) (x2 x3) ⟶ x1 x3)) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wrex x1 x2) (wex (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3)))) ⟶ (∀ x1 : ι → ο . ∀ x2 : ι → ι → ο . wb (wreu x1 x2) (weu (λ x3 . wa (wcel (cv x3) (x2 x3)) (x1 x3)))) ⟶ x0) ⟶ x0 |
|