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


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