apply Exists.elim h2
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))