Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ x3 ∈ x0) ⟶ decode_c (encode_c x0 x1) x2 = x1 x2

as obj
-

as prop
880bf..^{decode_encode_c}

theory
HotG

stx
08e38..

address
TMYed..^{decode_encode_c}