Proofgold Term Root Disambiguation

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x1 x3 ⟶ inj x1 x2 x4 ⟶ inj x0 x2 (λ x5 . x4 (x3 x5))

as obj
-

as prop
05a66..^inj_comp

theory
HotG

stx
ea22c..

address
TMdMv..^inj_comp