feat: remove open_fresh_preserve_not_fvar

[lengyijun]

This PR remove open_fresh_preserve_not_fvar: because open_preserve_not_fvar is the stronger version of open_fresh_preserve_not_fvar

[chenson2018]

This looks good, though I think the statement of open_preserve_not_fvar will change as part of #579.

[lengyijun]

This looks good, though I think the statement of open_preserve_not_fvar will change as part of #579.

theorem openRec_fv_cases {M N: Term String} :
(i: Nat) ->
(openRec i N M).fv = M.fv \/
(openRec i N M).fv = M.fv ∪ N.fv := by
induction M with grind

But simply replace open_preserve_not_fvar to openRec_fv_cases, some grind will not work