exact ih h1_right_right
case right
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_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
⊢ List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) tl
no goals