induction E
D : Type
I : Interpretation D
E : Env
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E (def_ X xs)
case nil
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)

case cons
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V tail✝ (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) tail✝ (def_ X xs)
⊢ Holds D I V (head✝ :: tail✝) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs)