Proofgold Object

λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . If_i (x0 x2 (x1 x2)) (x1 x2) (canonical_elt x0 x2)

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

theory
HotG

name
canonical_elt_def

definition
PURwt..

Megalodon
canonical_elt_def

proofgold address
TMZLp..^{canonical_elt_def}

creator
4897 Pr6Pc../8a381..

owner
4897 Pr6Pc../8a381..

term root
cd4f6..