Proofgold Proposition

∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 x2 . finite x1 ⟶ nIn x2 x1 ⟶ x0 x1 ⟶ x0 (binunion x1 (Sing x2))) ⟶ ∀ x1 . finite x1 ⟶ x0 x1

type
prop

theory
HotG

name
finite_ind

proof
PUMXD..

Megalodon
finite_ind

proofgold address
TMX5g..^finite_ind

creator
12443 PrGxv../de9ec..

owner
12443 PrGxv../de9ec..

term root
c53cb..