apply holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (hd :: tl) d.F s2
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
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F
case h2
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
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h3
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
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)