Given a goal that is an instance of a propositional formula, this tactic will
prove the goal provided it is valid. A propositional formula is a term
containing only Boolean constants, Boolean-valued variables, Boolean
equalities, implications, conjunctions, disjunctions, negations and
Boolean-valued conditionals. An instance of a formula is the formula with one
or more of the variables replaced by terms of the same type. The tactic
accepts goals with or without universal quantifiers for the variables.