Quick correction. In class I used the form define-sort to define an enumerated data type. The correct form is define-datatypes. The type definitions for Lab and Var should be:
(declare-datatypes () ((L l1 l2 l3 l4 l5 l6 l?)))
(declare-datatypes () ((V X Y Z)))