no goals
α : Type u
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ dedup (replicate (n + 2) x) = [x]
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
  replicate_dedup n.succ_ne_zero]