| ∀ x0 : ο . ((∀ x1 x2 : ο . x1 ⟶ (x1 ⟶ x2) ⟶ x2) ⟶ (∀ x1 x2 : ο . x1 ⟶ x2 ⟶ x1) ⟶ (∀ x1 x2 x3 : ο . (x1 ⟶ x2 ⟶ x3) ⟶ (x1 ⟶ x2) ⟶ x1 ⟶ x3) ⟶ (∀ x1 x2 : ο . (wn x1 ⟶ wn x2) ⟶ x2 ⟶ x1) ⟶ (∀ x1 x2 : ο . wn ((wb x1 x2 ⟶ wn ((x1 ⟶ x2) ⟶ wn (x2 ⟶ x1))) ⟶ wn (wn ((x1 ⟶ x2) ⟶ wn (x2 ⟶ x1)) ⟶ wb x1 x2))) ⟶ (∀ x1 x2 : ο . wb (wo x1 x2) (wn x1 ⟶ x2)) ⟶ (∀ x1 x2 : ο . wb (wa x1 x2) (wn (x1 ⟶ wn x2))) ⟶ (∀ x1 x2 x3 : ο . wb (wif x1 x2 x3) (wo (wa x1 x2) (wa (wn x1) x3))) ⟶ (∀ x1 x2 x3 : ο . wb (w3o x1 x2 x3) (wo (wo x1 x2) x3)) ⟶ (∀ x1 x2 x3 : ο . wb (w3a x1 x2 x3) (wa (wa x1 x2) x3)) ⟶ (∀ x1 x2 : ο . wb (wnan x1 x2) (wn (wa x1 x2))) ⟶ (∀ x1 x2 : ο . wb (wxo x1 x2) (wn (wb x1 x2))) ⟶ wb wtru ((∀ x1 . wceq (cv x1) (cv x1)) ⟶ ∀ x1 . wceq (cv x1) (cv x1)) ⟶ wb wfal (wn wtru) ⟶ (∀ x1 x2 x3 : ο . wb (whad x1 x2 x3) (wxo (wxo x1 x2) x3)) ⟶ (∀ x1 x2 x3 : ο . wb (wcad x1 x2 x3) (wo (wa x1 x2) (wa x3 (wxo x1 x2)))) ⟶ (∀ x1 : ι → ο . wb (wex x1) (wn (∀ x2 . wn (x1 x2)))) ⟶ (∀ x1 : ι → ο . wb (wnf x1) (wex x1 ⟶ ∀ x2 . x1 x2)) ⟶ x0) ⟶ x0 |
|