Proofgold Proposition

∀ x0 x1 . prim1 x1 (1216a.. (b5c9f.. x0 x0) (λ x2 . bij x0 x0 (f482f.. x2))) ⟶ explicit_Group_inverse (1216a.. (b5c9f.. x0 x0) (λ x3 . bij x0 x0 (f482f.. x3))) (λ x3 x4 . 0fc90.. x0 (λ x5 . f482f.. x4 (f482f.. x3 x5))) x1 = 0fc90.. x0 (inv x0 (f482f.. x1))

type
prop

theory
HoTg

name
-

proof
PUK9H..

Megalodon
-

proofgold address
TMYVP..

creator
4803 PrGxv../f527f..

owner
4803 PrGxv../f527f..

term root
829f8..