Goal:
  
  A : Type
  B : Type
  C : Type
  P : A → B → C → Type
  ls : list ((A × B) × C)
  ============================
   (All (λ '(a, b, c), P a b c) ls <~>
    All (λ abc : (A × B) × C, P abc.1.1 abc.1.2 abc.2) ls)


DEBUG:Going to execute:
split; induction 1