exact h1_1_1 c1
case neg.h.h1
F : Formula
v u : VarName
F' : Formula
h1_1_x : VarName
h1_1_phi : Formula
h1_1_v h1_1_t : VarName
binders : Finset VarName
h2 : h1_1_t ∉ binders
h1_1_1 : ¬h1_1_v = h1_1_x → ¬isFreeIn h1_1_v h1_1_phi
c1 : ¬h1_1_v = h1_1_x
⊢ ¬isFreeIn h1_1_v h1_1_phi
no goals