Proofgold Proposition

∀ x0 x1 : ι → ο . wceq (cseqom x0 x1) (cima (crdg (cmpt2 (λ x2 x3 . com) (λ x2 x3 . cvv) (λ x2 x3 . cop (csuc (cv x2)) (co (cv x2) (cv x3) x0))) (cop c0 (cfv x1 cid))) com)

type
prop

theory
SetMM

name
df_seqom

proof
PUR6R..

Megalodon
-

proofgold address
TMUjZ..

creator
36396 PrCmT../f03f2..

owner
36396 PrCmT../f03f2..

term root
6d176..