Proofgold Proposition

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

type
prop

theory
HotG

name
quotient_prop2

proof
PURwt..

Megalodon
quotient_prop2

proofgold address
TMSQA..^{quotient_prop2}

creator
4897 Pr6Pc../d32d6..

owner
4897 Pr6Pc../d32d6..

term root
54b14..