Goal:
  
  A : Type
  B : Type
  P : A → B → Type
  l : list A
  l' : list B
  HF : All2 P l l'
  ============================
   (Alli
      (λ (i : nat) (x : A),
         ∑ y : B, (nth_error l i = Some x ∧ nth_error l' i = Some y) × P x y)
      0 l)


DEBUG:Going to execute:
induction HF; constructor