new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)

Removed unnecessary and problematic trivial lemma from HOL-Algebra

proper executable file;