Proofgold Proposition

∀ x0 x1 . set_of_pairs x0 ⟶ set_of_pairs x1 ⟶ (∀ x2 x3 . iff (In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) x0) (In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) x1)) ⟶ x0 = x1

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
set_of_pairs_ext

proofgold address
TMXzS..^{set_of_pairs_ext}

creator
1627 PrGxv../d5b79..

owner
1627 PrGxv../d5b79..

term root
dc859..