cases E_ih_1
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1 : d ∈ E_tl ∧ name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
left✝ : d ∈ E_tl
right✝ : name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length