Goal:
    A : Type  P : nat → A → Type  Q : A → Type  k : nat  l : list A
  ============================
   (Alli P k l → All Q l → Alli (λ (k : nat) (x : A), P k x × Q x) k l)


DEBUG:Going to execute:
induction 1; constructor; try inversion X0