proposition: Lemma Forall_rect : forall (Q : list A -> Type), Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l.
proof: Proof. intros Q H H' l; induction l; intro; [|eapply H', Forall_inv]; eassumption. Qed.
imports: PeanoNat