unfold Instantiation.comp
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑(σ.comp σ')) xs)
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ pred_ X (List.map (↑σ) (List.map (↑σ') xs)) = pred_ X (List.map (↑⟨↑σ ∘ ↑σ', ⋯⟩) xs)