Goal:
    A : Type  B : Type  C : Type  P : A → B → C → Type  c : C  ls1 : list C
  ============================
   (∀ (ls2 : list A) (ls3 : list B),
      c :: ls1 ≠ [] ∨ #|ls2| = #|ls3|
      → All (λ z : C, All2 (λ (x : A) (y : B), P x y z) ls2 ls3) (c :: ls1)
        → All2 (λ (x : A) (y : B), All (P x y) (c :: ls1)) ls2 ls3)


DEBUG:Going to execute:
move  =>ls2 ls3 _