| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x5 x8 x9)) (x3 x4 x5 x8 x9 x6 = x3 x4 x5 x8 x9 x7)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12)) |
|
| type |
|---|
| (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → (ι → ι → ι) → ο |
|
|
| name |
|---|
| MetaCat_coequalizer_p |
|
|
|
|
|
|
|