Proofgold Proposition

∀ x0 x1 : ι → ο . wb (wirreflexive x0 x1) (wa (wss x1 (cxp x0 x0)) (wral (λ x2 . wn (wbr (cv x2) (cv x2) x1)) (λ x2 . x0)))

type
prop

theory
SetMM

name
df_irreflexive

proof
PUVbx..

Megalodon
-

proofgold address
TMQpn..

creator
36378 PrCmT../b3302..

owner
36378 PrCmT../b3302..

term root
d3821..