cases a1
case refine'_1.a.a.h1.h3
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
a1 : H = forall_ t (fastReplaceFree v t P.not_) ∨ H ∈ Δ
⊢ ¬isFreeIn t H
case refine'_1.a.a.h1.h3.inl
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
h✝ : H = forall_ t (fastReplaceFree v t P.not_)
⊢ ¬isFreeIn t H

case refine'_1.a.a.h1.h3.inr
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
h✝ : H ∈ Δ
⊢ ¬isFreeIn t H