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


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