intro E1 h1_1
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ 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
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)