| ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 x4 . (∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x5 = x1 x6 ⟶ x5 = x6) ⟶ not (∃ x5 . and (x5 ∈ x0) (x1 x5 = x2)) ⟶ x4 ∈ ordsucc x0 ⟶ ((x3 = x0 ⟶ ∀ x5 : ο . x5) ⟶ x3 ∈ x0) ⟶ If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 |
|
|
|
|
|
|
|
|
|
|