Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 x4 . ∀ x5 x6 : ι → ι . explicit_Nats x0 x1 x2 ⟶ bij x0 x3 x6 ⟶ x6 x1 = x4 ⟶ (∀ x7 . prim1 x7 x0 ⟶ x6 (x2 x7) = x5 (x6 x7)) ⟶ explicit_Nats x3 x4 x5

as obj
-

as prop
0ef95..

theory
HoTg

stx
04fcb..

address
TMGVh..^{explicit_Nats_transfer}