:: deftheorem defines Trivial-CLSStruct CLVECT_1:def 6 :
Trivial-CLSStruct = CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #);