Binary feature that returns zero iff a certain Taclet app has not already
been performed. Contrary to NonDuplicateAppFeature, this feature
is also able to handle failing meta-constructs correctly (these constructs
return equal, but not identical formulas in case of a failure), but is less
efficient.