make affinely_True_emp more useful, and make absorbingly lemmas consistent

Merged Ralf Jung requested to merge ralf/bi-lemmas into master

Factored out from !794 (merged)

Merge request reports