simp at a1
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
⊢ Holds D I V E H'
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ Holds D I V E H'