∀ {α : Type u_1} (motive : (x x_1 : List (List α)) → List.Forall₂ (fun x1 x2 => x1.Perm x2) x x_1 → Prop)
  (x x_1 : List (List α)) (x_2 : List.Forall₂ (fun x1 x2 => x1.Perm x2) x x_1),
  (∀ (a : Unit), motive [] [] ⋯) →
    (∀ (head : List α) (tail : List (List α)) (head_1 : List α) (tail_1 : List (List α)) (h₁ : head.Perm head_1)
        (h₂ : List.Forall₂ (fun x1 x2 => x1.Perm x2) tail tail_1), motive (head :: tail) (head_1 :: tail_1) ⋯) →
      motive x x_1 x_2