case _ c1 =>
  unfold IsMetaVarOrAllDefInEnv at h1
  simp at h1
  cases h1
  case inl c2 =>
    contradiction
  case inr c2 =>
    unfold sub at E_ih
    simp only [← E_ih c2]
    apply holds_coincide_meta_var
    unfold Formula.metaVarSet
    simp
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
no goals