Proofgold Proposition

∀ x0 x1 . x1 ∈ prim4 (ordsucc x0) ⟶ ∀ x2 : ο . (x1 ∈ prim4 x0 ⟶ x2) ⟶ (x0 ∈ x1 ⟶ setminus x1 (Sing x0) ∈ prim4 x0 ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
In_Power_ordsucc_cases_impred

proof
PUfcG..

Megalodon
-

proofgold address
TMQV5..

creator
14561 Pr4zB../1d36e..

owner
14561 Pr4zB../1d36e..

term root
eda78..