simp at c2
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q