simp only [all_def_in_env] at h2
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, a✝¹ = d.name ∧ a✝.length = d.args.length
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)