Proofgold Proposition

wceq ctopon (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wceq (cv x0) (cuni (cv x1))) (λ x1 . ctop)))

type
prop

theory
SetMM

name
df_topon

proof
PUaM6..

Megalodon
-

proofgold address
TMai9..

creator
36385 PrCmT../ec088..

owner
36385 PrCmT../ec088..

term root
8943e..