# Rewriting inside quantified propositions in Coq?

Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:

Goal forall (xs : list nat) (ys : list nat),
(forall x, In x (xs ++ ys) -> x < 10) -> True.
Proof.
intros.


makes the context look like

A: Type
xs, ys: list nat
H: forall x : nat, In x (xs ++ ys) -> x < 10


Now, recall that

in_app_iff
: forall (A : Type) (l l' : list A) (a : A),
In a (l ++ l') <-> In a l \/ In a l'


However, rewrite in_app_iff in H. gives me an error:

Found no subterm matching "In ?y (?l ++ ?l0)" in the current goal.


I want it to transform the context into

H: forall x : nat, (In x xs \/ In x ys) -> x < 10


I am aware that I can do this by first specializing x inside an assert environment or something, but it would be really nifty if I didn't have to do that.

Yes, the tactic setoid_rewrite lets you rewrite under binders. Here is the reference manual link.

From Coq Require Import List.
Goal forall (xs : list nat) (ys : list nat),
(forall x, In x (xs ++ ys) -> x < 10) -> True.
Proof.
intros xs ys H.


The context is

xs, ys : list nat
H : forall x : nat, In x (xs ++ ys) -> x < 10
========================= (1 / 1)
True


then writing

  setoid_rewrite in_app_iff in H.


gives you

xs, ys : list nat
H : forall x : nat, In x xs \/ In x ys -> x < 10
========================= (1 / 1)
True