simp only [sub] at E_ih
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)