Hello,

I have an inductive type that uses `list`

. When trying to prove things by induction on on it, I can’t manage to get an induction hypothesis for the elements of the `list`

:

```
Inductive things : Type :=
| B : bool -> things
| A : list things -> things.
Inductive is_true : things -> Prop :=
| Foo_B : forall b, b = true -> is_true (B b)
| Foo_A : forall ts, Forall is_true ts -> is_true (A ts).
Fixpoint is_trueb (t : things) : bool :=
match t with
| B b => b
| A ts => forallb is_trueb ts
end.
Lemma sound: ∀ t,
is_trueb t = true -> is_true t.
Proof.
induction t.
- (* B *) simpl. constructor. assumption.
- (* A *) (* I'm here *)
```

At this point I have to prove:

```
l : list things
============================
is_trueb (A l) = true → is_true (A l)
```

and I would ideally like to have a hypothesis of the form:

```
H : forall x, In x l -> is_trueb x = true -> is_true x
```

Any ideas how to go about this? Thanks!