∀ {α : Type u_1} {γ : Type u_2} (motive : List α → List γ → Prop) (x : List α) (x_1 : List γ),
  (∀ (x : List α), motive x []) → (∀ (x : List α) (b : γ) (u : List γ), motive x (b :: u)) → motive x x_1