Unable to split a conjunction in Hypothesis

Question

I have the following Hypothesis:

ls: list(R)

H: forall n : nat,
     0 <= INR n < 10 ->
     My_first_condition n
     /\forall x : R,
      In x ls ->
      My_second_condition x

What I would like to achieve is to be able to split H as two conditions:

ls: list(R)

H1: forall n : nat,
     0 <= INR n < 10 ->
     My_first_condition n

H2: forall x : R,
    In x ls ->
    My_second_condition x

To do this, I tried to use destruct H but I got the following error:

Unable to find an instance for the variables n.

Does anyone know why it happens and what would be a solution ?

user_1633770 · Answer

You need parentheses around the forall:

(forall n : nat, ...) /\
(forall x : R, ...)

Right now, Coq interprets what you wrote as

forall n : nat, (
  ... /\ forall x : R, ...
)