Goal:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : A → B → Type
  l : list A
  l' : list B
  a : All2 R l l'
  ============================
   (All2 R' l l' <~> All2_dep (λ (x : A) (y : B) (_ : R x y), R' x y) a)


DEBUG:Going to execute:
split; [ induction a; inversion 1 | induction 1 ]; constructor