Goal:
    A : Type  P : A → Type  Q : nat → A → Type  l : list A  H : All P l
  ============================
   (∀ n : nat, (∀ (n0 : nat) (x : A), P x → Q n0 x) → Alli Q n l)


DEBUG:Going to execute:
induction H; constructor