Goal:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  H : ∀ (n : nat) (x : A) (y : B), R n x y
  n : nat
  l : list A
  l' : list B
  ============================
   (#|l| = #|l'| → All2i R n l l')


DEBUG:Going to execute:
induction l in n, l' |- *; destruct l'; simpl; try discriminate;
            intros; constructor