∀ x0 . x0 ∈ prim4 3 ⟶ ∀ x1 : ο . (x0 = 0 ⟶ x1) ⟶ (x0 = 1 ⟶ x1) ⟶ (x0 = Sing 1 ⟶ x1) ⟶ (x0 = 2 ⟶ x1) ⟶ (x0 = Sing 2 ⟶ x1) ⟶ (x0 = UPair 0 2 ⟶ x1) ⟶ (x0 = UPair 1 2 ⟶ x1) ⟶ (x0 = 3 ⟶ x1) ⟶ x1 |
|
|
|
name |
---|
In_Power_3_cases_impred |
|
|
|
|
|
|
|