Proofgold Term Root Disambiguation

∀ 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

as obj
-

as prop
51150..^{set_of_pairs_ext}

theory
HF

stx
89549..

address
TMQF7..^{set_of_pairs_ext}