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. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html