| ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ο . ∀ x4 x5 . wceq (cmpt3 x0 x1 x2 x3) (copab (λ x6 x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . wa (wceq (cv x6) (cotp (cv x8) (cv x9) (cv x10))) (wceq (cv x7) (x3 x8 x9 x10))) (x2 x8 x9)) (λ x9 . x1 x8 x9 x5)) (λ x8 . x0 x8 x4 x5))) |
|