induction E
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ X xs) ↔ Holds D I V E (def_ X (List.map σ xs))
case nil
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))

case cons
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I (V ∘ σ) tail✝ (def_ X xs) ↔ Holds D I V tail✝ (def_ X (List.map σ xs))
⊢ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs) ↔ Holds D I V (head✝ :: tail✝) (def_ X (List.map σ xs))