∀ {ι : Type u_1} (motive : (x : List ι) → x.Nodup → Prop) (x : List ι) (x_1 : x.Nodup),
  (∀ (x : [].Nodup), motive [] x) → (∀ (a : ι) (l : List ι) (hl : (a :: l).Nodup), motive (a :: l) hl) → motive x x_1