no goals
ι : Type ?u.12121
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
⊢ [] = replicate (length []) a ↔ ∀ (b : α), b ∈ [] → b = a
simp
no goals
ι : Type ?u.12121
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ b :: l = replicate (length (b :: l)) a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a
simp [eq_replicate_length]