Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x2 ⟶ and (setsum_p x4) (In (ap x4 0) x0)) ⟶ (∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4)) ⟶ x3) ⟶ x3

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
PiE_impred

proofgold address
TMVhj..^PiE_impred

creator
1627 PrGxv../51ebf..

owner
1627 PrGxv../51ebf..

term root
c2057..