Proofgold Proposition

combinator = λ x1 . ∀ x2 : ι → ο . x2 (Inj0 0) ⟶ x2 (Inj0 (Power 0)) ⟶ (∀ x3 x4 . x2 x3 ⟶ x2 x4 ⟶ x2 (Inj1 (setsum x3 x4))) ⟶ x2 x1

type
prop

theory
hf axiom

name
-

proof
-

Megalodon
combinator_def

proofgold address
-

creator

owner

term root
24d3f..