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


DEBUG:Going to execute:
revert L2; induction L1; cbn