Proofgold Proposition

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

type
prop

theory
HotG

name
canonical_elt_eq

proof
PURwt..

Megalodon
canonical_elt_eq

proofgold address
TMPA9..^{canonical_elt_eq}

creator
4897 Pr6Pc../1368a..

owner
4897 Pr6Pc../1368a..

term root
77a0b..