diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md index 9df7b6fde..47e98f2fa 100644 --- a/prover/strategies/simplification.md +++ b/prover/strategies/simplification.md @@ -563,7 +563,7 @@ We define a similar strategy for quantified implication contexts: rule removeTrivialEqualities(P, Ps) => P, removeTrivialEqualities(Ps) [owise] ``` -### Substitute Equals for equals +### Remove constraints ``` PHI /\ C => PSI