Proofgold Term Root Disambiguation

∀ 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

as obj
-

as prop
4367f..^{set_of_pairs_ext}

theory
HotG

stx
08e38..

address
TMJxK..^{set_of_pairs_ext}