intro a
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
⊢ ∀ (a : VarName), a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset
case a
c : Char
X : DefName
xs : List VarName
σ : VarName → VarName
a : VarName
⊢ a ∈ (List.map σ xs).toFinset ↔ a ∈ Finset.image σ xs.toFinset