case conv_unfold d σ h2 =>
  obtain ⟨σ', a1⟩ := σ.2
  have s1 : IsMetaVarOrAllDefInEnv E d.F := def_in_well_formed_env_is_meta_var_or_all_def_in_env E d h1 h2
  simp only [← holds_sub D I V M E σ σ' meta_var_ d.F s1 a1]
  clear s1
  have s2 : d.name = d.name ∧ (List.map σ.val d.args).length = d.args.length
  simp
  simp only [← lem_4 D I V M E d d.name (List.map σ.val d.args) h1 h2 s2]
  clear s2
  have s3 : d.F.metaVarSet = ∅ := no_meta_var_imp_meta_var_set_is_empty d.F d.args d.nf
  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]
  clear s3
  apply holds_coincide_var D I (Function.updateListITE V d.args (List.map V (List.map σ.val d.args))) (V ∘ σ.val) M E d.F d.args d.nf
  intro v a2
  simp
  exact Function.updateListITE_map_mem V (V ∘ σ.val) d.args v a2
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)
no goals