| λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (and (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x1) (KPair_alt7 x4 x6 ∈ x3) ⟶ x5) ⟶ x5) (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (KPair_alt7 x6 x4 ∈ x3) ⟶ x5) ⟶ x5)) (∀ x4 x5 x6 x7 . KPair_alt7 x4 x5 ∈ x3 ⟶ KPair_alt7 x6 x7 ∈ x3 ⟶ iff (x4 = x6) (x5 = x7)) ⟶ x2) ⟶ x2 |
|