TAUT_TACtautLib.TAUT_TAC : tacticTautology checker. Proves propositional goals (and instances of them).
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.
Fails if the conclusion of the goal is not an instance of a propositional formula or if the instance is not a valid formula.