obtain ⟨σ', a1⟩ := σ.2
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
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ 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
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)