induction E
E : Env
h1 : E.WellFormed
⊢ E.Nodup
case nil
h1 : Env.WellFormed []
⊢ Env.Nodup []

case cons
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Env.WellFormed tail✝ → Env.Nodup tail✝
h1 : Env.WellFormed (head✝ :: tail✝)
⊢ Env.Nodup (head✝ :: tail✝)