Proofgold Proposition

∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 . x0 x1 x1 ⟶ canonical_elt x0 x1 = canonical_elt x0 (canonical_elt x0 x1)

type
prop

theory
HotG

name
canonical_elt_idem

proof
PURwt..

Megalodon
canonical_elt_idem

proofgold address
TMNx4..^{canonical_elt_idem}

creator
4897 Pr6Pc../d023f..

owner
4897 Pr6Pc../d023f..

term root
f360e..