Goal:
  
  A : Type
  B : Type
  R : A → B → Prop
  R' : A → B → Prop
  l : list A
  l' : list B
  a : Forall2 R l l'
  ============================
   (Forall2 R' l l' ↔ Forall2_dep (λ (x : A) (y : B) (_ : R x y), R' x y) a)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>