induction E
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
d : Definition
name : DefName
args : List VarName
h1 : E.WellFormed
h2 : d ∈ E
h3 : name = d.name ∧ args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M E d.F ↔ Holds D I V M E (def_ name args)
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
h1 : Env.WellFormed []
h2 : d ∈ []
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M [] d.F ↔ Holds D I V M [] (def_ name args)

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  Env.WellFormed tail✝ →
    d ∈ tail✝ →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tail✝ d.F ↔ Holds D I V M tail✝ (def_ name args))
h1 : Env.WellFormed (head✝ :: tail✝)
h2 : d ∈ head✝ :: tail✝
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (head✝ :: tail✝) d.F ↔
    Holds D I V M (head✝ :: tail✝) (def_ name args)