Logic: All_In can't expand nested forall

Question

I am facing a pretty strange problem: coq doesn't want to move forall variable into the context.

In the old times it did:

Example and_exercise :
  forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
Proof.
  intros n m.

It generates:

n, m : nat
============================
n + m = 0 -> n = 0 /\ m = 0

But when we have forall inside forall, it doesn't work:

(* Auxilliary definition *)
Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  (* ... *)

Lemma All_In :
  forall T (P : T -> Prop) (l : list T),
    (forall x, In x l -> P x) <->
    All P l.
Proof.
  intros T P l. split.
  - intros H.

After this we get:

T : Type
P : T -> Prop
l : list T
H : forall x : T, In x l -> P x
============================
All P l

But how to move x outside of H and destruct it into smaller pieces? I tried:

destruct H as [x H1].

But it gives an error:

Error: Unable to find an instance for the variable x.

What is it? How to fix?

Answer 1

The problem is that forall is nested to the left of an implication rather than the right. It does not make sense to introduce x from a hypothesis of the form forall x, P x, just like it wouldn't make sense to introduce the n in plus_comm : forall n m, n + m = m + n into the context of another proof. Instead, you need to use the H hypothesis by applying it at the right place. I can't give you the answer to this question, but you might want to refer to the dist_not_exists exercise in the same chapter.