cases h1
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
case intro
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs