| ∀ x0 x1 x2 x3 x4 . (x0 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ equip u5 (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) |
|