simp only [← s1] at a1
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)