Goal:
  
  A : Type
  B : Type
  k : nat
  Q : nat → A → Type
  R : nat → A → B → Type
  l : list A
  l' : list B
  ============================
   (Alli Q k l
    → All2i R k l l'
      → All2i (λ (i : nat) (x : A) (y : B), Q i x × R i x y) k l l')


DEBUG:Going to execute:
move  =>+ h; elim : h  => [n|n x y xs ys r rs ih] q;
            depelim ltac:(q)