Proofgold Proposition

∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . x3 ∈ x0 ⟶ inv x0 x2 (x2 x3) = x3

type
prop

theory
HotG

name
inj_linv_coddep

proof
PUL8Q..

Megalodon
-

proofgold address
TMTFj..

creator
4882 Pr6Pc../e6a08..

owner
4882 Pr6Pc../e6a08..

term root
f9fc2..