exact h5 H c1
P Q : Formula
v t : VarName
Δ : Set Formula
h2 : IsDeduct (Δ ∪ {fastReplaceFree v t P}) Q
h3 : ¬occursIn t P
h4 : ¬occursIn t Q
h5 : ∀ H ∈ Δ, ¬isFreeIn t H
h1 : IsDeduct Δ (forall_ v P.not_).not_
H : Formula
c1 : H ∈ Δ
⊢ ¬isFreeIn t H
no goals