The theorems and tactics here are for eliminating occurrences of 'tt' and 'ff' in boolean expressions and simplifying boolean atomic predicates that have constant arguments.