Proofgold Proposition

∀ x0 x1 : ι → ο . wceq (cafv x0 x1) (cif (wdfat x0 x1) (cio (λ x2 . wbr x0 (cv x2) x1)) cvv)

type
prop

theory
SetMM

name
df_afv

proof
PUYnf..

Megalodon
-

proofgold address
TMQrR..

creator
36378 PrCmT../609d7..

owner
36378 PrCmT../609d7..

term root
65233..