Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . symmetric_i x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1

as obj
-

as prop
2acec..^{symmetric_i_E}

theory
HF

stx
b6147..

address
TMQ3f..^{symmetric_i_E}