induction E1
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V (E1 ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
case nil
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

case cons
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (tail✝ ++ E) →
    (Holds D I V (tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (head✝ :: tail✝ ++ E)
⊢ Holds D I V (head✝ :: tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)