Proofgold Object

λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . and (x0 x2 x2) (x2 = canonical_elt_def x0 x1 x2)

type
(ι → ι → ο) → (ι → ι) → ι → ο

theory
HotG

name
quotient_def

definition
PURwt..

Megalodon
quotient_def

proofgold address
TMQgk..^quotient_def

creator
4897 Pr6Pc../39332..

owner
4897 Pr6Pc../39332..

term root
612d4..