Proofgold Proposition

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

type
prop

theory
HotG

name
set_of_pairs_ext

proof
PUdQg..

Megalodon
set_of_pairs_ext

proofgold address
TMJd1..^{set_of_pairs_ext}

creator
4899 Pr6Pc../ed1de..

owner
4899 Pr6Pc../ed1de..

term root
a6a9b..