induction E
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
name : DefName
args : List VarName
h1 : Holds D I V M E (def_ name args)
⊢ ∃ d ∈ E, name = d.name ∧ args.length = d.args.length
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V M tail✝ (def_ name args) → ∃ d ∈ tail✝, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (head✝ :: tail✝) (def_ name args)
⊢ ∃ d ∈ head✝ :: tail✝, name = d.name ∧ args.length = d.args.length