Proofgold Proposition

∀ x0 : ι → ο . x0 (Inj0 0) ⟶ x0 (Inj0 (Power 0)) ⟶ (∀ x1 x2 . combinator x1 ⟶ x0 x1 ⟶ combinator x2 ⟶ x0 x2 ⟶ x0 (Inj1 (setsum x1 x2))) ⟶ ∀ x1 . combinator x1 ⟶ x0 x1

type
prop

theory
HF

name
-

proof
PUJuQ..

Megalodon
combinator_ind

proofgold address
TMe1C..^{combinator_ind}

creator
2336 PrGxv../40387..

owner
2336 PrGxv../40387..

term root
598b1..