cases l
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
⊢ l = []
case nil
m n : Nat
nodup : List.Nodup []
⊢ [] = []

case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []