# Strengthening inductive hypothesis for lists?

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
``````

You may have a look at Nested Inductive Types.

1 Like