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