Goal:
    A : Type  B : Type  L1 : list A  L2 : list B  P : A → B → Type
  ============================
   (#|L1| = #|L2|
    → (∀ (n : nat) (x1 : A) (x2 : B),
         n < #|L1|
         → nth_error L1 n = Some x1 → nth_error L2 n = Some x2 → P x1 x2)
      → All2 P L1 L2)


DEBUG:Going to execute:
revert L2; induction L1