simp only [c1_left]
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = X
no goals