Proofgold Proposition

∀ x0 . x0 ∈ int ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ omega ⟶ x0 = minus_SNo (ordsucc x2) ⟶ x1) ⟶ (x0 = 0 ⟶ x1) ⟶ (∀ x2 . x2 ∈ omega ⟶ x0 = ordsucc x2 ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
int_3_cases

proof
PUfrJ..

Megalodon
int_3_cases

proofgold address
TMLh3..^int_3_cases

creator
27869 PrQUS../551d3..

owner
27869 PrQUS../551d3..

term root
67b16..