Proofgold Proposition

∀ x0 x1 : ι → ο . wceq (caltxp x0 x1) (cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (caltop (cv x3) (cv x4))) (λ x4 . x1)) (λ x3 . x0)))

type
prop

theory
SetMM

name
df_altxp

proof
PUKaw..

Megalodon
-

proofgold address
TMSHr..

creator
36383 PrCmT../4868a..

owner
36383 PrCmT../4868a..

term root
406e3..