haskell - Haskell 自定义函数的归纳证明

Question

我正在研究归纳，我有一些问题要弄清楚如何完成我的“destutter”函数的归纳证明，该函数删除列表中的连续重复项：

destutter [] = []                                          Destrutter.1
destutter (x:xs) = x : (destutter (dropWhile (== x) xs))   Destrutter.2

这是假设：

destutter (destutter xs) == destutter xs

这是我到目前为止所做的：

证明基本情况（空列表）

-- BASE CASE --

Left side:
destutter (destutter xs)
== {- xs = [] -}
destutter (destutter [])
== {- Destrutter.1, destutter [] = [] -}
destutter ([])
== {- Destrutter.1, destutter [] = [] -}
[]

Right side:
destrutter xs
== {- xs = [] -}
destrutter []
== {- Destrutter.1, destutter [] = [] -}
[]

Left side == Right side -> Proved

证明一般情况：

-- GENERAL CASE --

Assumption: destutter (destutter xs) == destutter xs
Claim: destutter (destutter (x:xs)) == destutter (x:xs)

destutter (destutter (x:xs))
== {- Destrutter.2, destutter (x:xs) = x : (destutter (dropWhile (== x) xs)) -}
destutter (x: (destutter (dropWhile (== x) xs)))
== {- Destrutter.2, destutter (x:xs) = x : (destutter (dropWhile (== x) xs)) -}
x : (destrutter (dropWhile (==x) (destutter (dropWhile (== x) xs))))

这是我遇到一些问题的地方：我不知道如何使用假设来达到：

destrutter (x:xs)

我尝试了不同的方法，但似乎没有一种方法是正确的。我做的步骤好吗？我的推理方式正确吗？