simp
case h1
d hd : Definition
tl : List Definition
ih : Env.WellFormed tl → d ∈ tl → IsMetaVarOrAllDefInEnv tl d.F
h2 : d = hd ∨ d ∈ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
⊢ hd :: tl = [hd] ++ tl
no goals