Proofgold Proposition

set_of_pairs = λ x1 . ∀ x2 . In x2 x1 ⟶ ∃ x3 x5 . x2 = lam 2 (λ x8 . If_i (x8 = 0) x3 x5)

type
prop

theory
hf axiom

name
-

proof
-

Megalodon
set_of_pairs_def

proofgold address
-

creator

owner

term root
4ad57..