exact isFreeIn_imp_occursIn t phi h1_right
case h.e'_2.h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
c1 : v = x
h1_right : isFreeIn t phi
⊢ occursIn t phi
no goals