case intro h3_left h3_right =>
  exfalso
  exact c1 h3_left h3_right
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (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))
h1_right_right : Env.WellFormed tl
s1 : Env.Nodup (d :: tl)
s2 : ∃ E1, d :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, d.name = d'.name → d.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl d.F
c1 : name = d.name → ¬args.length = d.args.length
h3_left : name = d.name
h3_right : args.length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (d :: tl) d.F ↔ Holds D I V M tl (def_ name args)
no goals