[lmq-1] is entailed by [tht-1]

[wceusters]

So [lmq-1] can be removed from the axioms and added to the list of theorems (if there is such list).

[alanruttenberg]

Fixed in the source. Next version won't have lmq-1.