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