| ∀ x0 : ι → ι → ο . ∀ x1 x2 . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ x0 x3 x2) ⟶ (∀ x3 . x3 ∈ binunion x1 (Sing x2) ⟶ ∀ x4 . x4 ∈ binunion x1 (Sing x2) ⟶ x0 x3 x4 ⟶ x0 x4 x3) ⟶ ∀ x3 . x3 ∈ binunion x1 (Sing x2) ⟶ ∀ x4 . x4 ∈ binunion x1 (Sing x2) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4 |
|