no goals
ι : Type ?u.18245
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ n, L = replicate n a
simp only [eq_replicate, subset_def, mem_singleton, exists_eq_left']