:: deftheorem defines VERUM MODAL_1:def 15 :
VERUM = (elementary_tree 0) --> [0,0];