Default Simp.Context for simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions.

Instances For

    Default discharge? function for simpIf methods. It only uses hypotheses from the local context. It is effective after a case-split.

    Instances For

      Return the condition of an if expression to case split.