I have a proof starting with `Forall`

(not `forall`

). Locate points me to `Coq.Lists.Forall`

, this is new to me, I can't destruct and can't induce over it, is there any resources (paper, books, etc) for working with this type? I took a look at LF Lists chapter but it doens't say nothing about this `Forall`

It's an inductive type that lives in `Prop`

so you cannot destruct it or perform induction on it to produce relevant things (in `Type`

or `Set`

).

You can use `destruct`

or `induction`

if your goal lives in `Prop`

.

Here is the definition:

```
Inductive Forall : list A -> Prop :=
| Forall_nil : Forall nil
| Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
```

I would assume you could do induction on the list?

If you must land in `Type`

then you can perform induction on the list argument and use `inversion`

for instance.

you can also use lemma `Forall_forall`

or `induction H using Forall_rect`

may work (with H the Forall hypothesis)

I can do induction on list, yeah I will try that, thanks Ana!

Thanks Théo for the explanation, now makes much more sense to be why I couldn't use induction on this Forall. And Thanks @Gaëtan Gilbert too , I will take note on this lemma, it may be useful!

Last updated: Jan 28 2023 at 05:02 UTC