Goal:
  
  A : Type
  I : Type
  B : Type
  P : I → B → B → Type
  i : list I
  l : list A
  l' : list A
  f : A → B
  ============================
   (OnOne2All (λ i : I, on_Trel (P i) f) i l l'
    → OnOne2All P i (map f l) (map f l'))


DEBUG:Going to execute:
induction 1; simpl; constructor; try congruence