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


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2