case struct_2_ Δ' H _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  cases a1
  case _ a1_left a1_right =>
    simp at a2
    cases a2
    case _ a2 =>
      simp only [a2]
      exact a1_left
    case _ a2 =>
      exact a1_right H' a2
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
no goals