no goals
e : List Nat
h : e ≠ []
⊢ mergeIdem e ≠ []
induction e using List.two_step_induction with
| empty => simp_all
| single => simp [mergeIdem, mergeIdem.loop]
| step => simp [mergeIdem, mergeIdem.loop] at *; split <;> simp_all
no goals
case empty
h : [] ≠ []
⊢ mergeIdem [] ≠ []
simp_all
no goals
case single
a✝ : Nat
h : [a✝] ≠ []
⊢ mergeIdem [a✝] ≠ []
simp [mergeIdem, mergeIdem.loop]
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : ¬mergeIdem.loop b✝ l✝ = []
h : True
⊢ ¬(if a✝¹ = b✝ then mergeIdem.loop a✝¹ l✝ else a✝¹ :: mergeIdem.loop b✝ l✝) = []
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : b✝ :: l✝ ≠ [] → mergeIdem (b✝ :: l✝) ≠ []
h : a✝¹ :: b✝ :: l✝ ≠ []
⊢ mergeIdem (a✝¹ :: b✝ :: l✝) ≠ []
simp [mergeIdem, mergeIdem.loop] at *
no goals
case step
a✝¹ b✝ : Nat
l✝ : List Nat
a✝ : ¬mergeIdem.loop b✝ l✝ = []
h : True
⊢ ¬(if a✝¹ = b✝ then mergeIdem.loop a✝¹ l✝ else a✝¹ :: mergeIdem.loop b✝ l✝) = []
split <;> simp_all