Added tactics for pulling universal quantification to the left of an
entailment relation for both logics with a later operator, and for BI
logics. This crudely solves the expression problem.