Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . In x5 x2x3 x5 = x4 x5)If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0 = If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0
as obj
-
as prop
dbaea..nat_primrec_r
theory
HF
stx
e311e..
address
TMU2V..nat_primrec_r