Proofgold Proposition

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

type
prop

theory
HotG

name
explicit_Nats_transfer

proof
PUefP..

Megalodon
explicit_Nats_transfer

proofgold address
TMbdd..^{explicit_Nats_transfer}

creator
4913 Pr6Pc../fa367..

owner
4913 Pr6Pc../fa367..

term root
3a371..