I'm sure there's still something I miss about Coq/ssr: sometimes I don't manage to rewrite something as I would like because of "The LHS of ... (...) does not match any subterm of the goal".

For example:

```
From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp.
Section FooOk.
Variable A B C D E: Prop.
Hypothesis c: C.
Hypothesis d: D.
Lemma ok: A -> ~ (B -> C /\ D) -> E.
Proof.
rewrite not_implyP.
rewrite not_andP.
Admitted.
End FooOk.
Section FooBad.
Lemma bad: ~ (forall P: Prop, P -> (exists Q: Prop, Q -> P /\ Q)).
Proof.
rewrite -existsNE.
rewrite not_implyP. (* FIXME: why !? *)
(* here I'm supposed to go on with migrating ~ inside *)
End FooBad.
```

"inside" means that you want to rewrite under a binder, which in general requires an additional justification.

Is the quantification a blocking binder and how can I go through?

I know how to go inside a bigop, but this much more simple situation didn't look like it would warrant this type of consideration.

yes, the quantification is a blocking binder

but I don't know if e.g. the non-ssreflect tactic `setoid_rewrite`

would ask for an extra proof here

How can I go through to push the ~ further inside? And when that's done, can I easily push it some more?

Last updated: Jan 29 2023 at 18:03 UTC