. apply Nat.lt_of_succ_lt_succ pf1
case self.pf1
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ n < length ?self.xs

case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique ?self.xs

case self.α
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Type u_1

case self.xs
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ List ?self.α

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get ?self.xs { val := n, isLt := ?self.pf1 } ∈ sieve bs ?self.xs
case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique xs

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs