simp only [holds_coincide_meta_var_no_meta_var D I (V ∘ σ.val) (fun (X' : MetaVarName) (V' : Valuation D) => Holds D I (V' ∘ σ') M E (meta_var_ X')) M E d.F s3]
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔ Holds D I (V ∘ ↑σ) M E d.F