unfold NoMetaVarAndAllFreeInList at h1
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ x y))
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ NoMetaVarAndAllFreeInList (List.map (↑σ) vs) (sub σ τ (eq_ x y))