feat(FullBeta, FullEta): generalize step_not_fv

[lengyijun]

The PR prefer left side of Finset.subset_iff_notMem

1. Make the FullBeta.step_not_fv more powerful and reusable, N.fv ⊆ M.fv instead of w ∉ M.fv -> w ∉ N.fv
2. Make the FullEta.step_not_fv more accurate: fv never changes after FullEta

[chenson2018]

Small changes like this can seem self-explanatory, but you have opened multiple PRs in a short span with no description. It would be appreciated to add appropriate descriptions, as they can be very helpful down the line.

[chenson2018]

I appreciate the effort to keep these PRs small, but could you consolidate this and #578 into one PR? They seem to be the same idea that writing the subset is preferred direction of Finset.subset_iff_notMem. I'd grep for ∉ in this directory and see if there are any others.

[lengyijun]

Should we rename the lemma: step_not_fv looks on longer suitable

[chenson2018]

Should we rename the lemma: step_not_fv looks on longer suitable

Yes, but let's do the naming in a follow up PR to keep the diff clean. In general when I wrote this, I didn't follow the naming conventions well.

[lengyijun]

Should I squash 2 commits to 1 ?

[lengyijun]

Do we need to make the names the same on both sides?

Idea:

lemma step_fv_eq (step : M ⭢ηᶠ M') : M.fv = M'.fv := by

lemma step_fv_subset (step : M ⭢βᶠ N) : N.fv ⊆ M.fv := by

[chenson2018]

Should I squash 2 commits to 1 ?

It does not matter, as we have this repo configured to squash all commits upon merging.

[lengyijun]

What else do I need to do in this PR?

[chenson2018]

What else do I need to do in this PR?

What I would like is to merge in changes from your other PRs, then similarly update all other theorems where x ∉ ?_ appears in a hypothesis and the goal. As you already noted, some grind proofs will need to be adjusted.