Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . In x3 (Sep2 x0 x1 x2) ⟶ ∃ x4 . and (In x4 x0) (∃ x6 . and (In x6 (x1 x4)) (and (x3 = lam 2 (λ x9 . If_i (x9 = 0) x4 x6)) (x2 x4 x6)))

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
Sep2E

proofgold address
TMSQa..^Sep2E

creator
1627 PrGxv../72d87..

owner
1627 PrGxv../72d87..

term root
4f9cf..