cases h2_1_right
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
h2_1_right : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
left✝ : X = a.name
right✝ : xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)