constructor
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs ∧ ↑σ y ∈ List.map (↑σ) vs
case left
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ x ∈ List.map (↑σ) vs

case right
σ : Instantiation
τ : MetaInstantiation
x y : VarName
vs : List VarName
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ↑σ y ∈ List.map (↑σ) vs