Theorem: List.subperm_nil (LeanCamCombi/Mathlib/Data/List/Basic.lean)

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ l = [] → l <+~ []
Tactic:
rintro rfl
State after:
α : Type u_1
l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ [] <+~ []

State before:
α : Type u_1
l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ [] <+~ []
Tactic:
rfl
State after:
no goals