unfold Env.Nodup at ih
hd : Definition
tl : List Definition
ih : Env.WellFormed tl → Env.Nodup 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 : Env.WellFormed (hd :: tl)
⊢ Env.Nodup (hd :: tl)