assumption
α : Type u_1
inst✝ : DecidableEq α
_x✝ : (_ : List α) ×' List α
a✝¹ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y _x✝ →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x✝² x✝¹ : List α
a✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x✝², snd := x✝¹ } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x : α
xs ys : List α
x✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x :: xs, snd := ys } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
hterm : length (filter (fun a => decide ¬a ∈ ys) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
⊢ (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 { fst := xs, snd := ys }
    { fst := x :: xs, snd := ys }
no goals