simp
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : PredName
xs : List VarName
V : VarAssignment D
⊢ I.pred_var_ X (List.map (V ∘ σ) xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
no goals