unfold sub
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1 : x ∈ vs ∧ y ∈ vs
⊢ 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) (eq_ (↑σ x) (↑σ y))