Goal:
    A : Type  B : Type  R : A → B → Prop  l : list A  l' : list B
  ============================
   ((∀ (x : A) (y : B), R x y) → #|l| = #|l'| → Forall2 R l l')


DEBUG:Going to execute:
<coq-core.plugins.ltac::intro@1> $1