unfold Env.WellFormed at h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h1 : Env.WellFormed (hd :: tl)
h2 : d ∈ hd :: tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d ∈ hd :: tl
h1 :
  (∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False) ∧
    IsMetaVarOrAllDefInEnv tl hd.F ∧ Env.WellFormed tl
⊢ IsMetaVarOrAllDefInEnv (hd :: tl) d.F