feat(locallynameless): eta-postpone

[lengyijun]

5 version of eta-postpone theorems:

• transgen_postpone_eta_beta: if P →ηᶠ Q and Q →βᶠ R, then there is a term
  S with P ↠β+ S and S ↠ηᶠ R.
• commute_etastar_beta: if P ↠ηᶠ Q and Q ↠βᶠ R, then there is a term
  S with P ↠βᶠ S and S ↠ηᶠ R.
• semiDiamondCommute_eta_beta: if P →ηᶠ Q and Q ↠β+ R, then there is a term
  S with P ↠β+ S and S ↠ηᶠ R.
• diamondcommute_etaplus_betastar: if P ↠ηᶠ Q and Q ↠β+ R, then there is
  a term S with P ↠β+ S and S ↠ηᶠ R.
• eta_postpone: if P ↠βηᶠ Q, then there is a term S such that
  P ↠βᶠ S and S ↠ηᶠ Q.

Ai usage:
ParEta.lean and BetaNfLc.lean are generated by @Aristotle-Harmonic

[lengyijun]

@thomaskwaring Sorry for the wait. Could you please take a look at this PR?

[lengyijun]

This PR is independent of #860. However, when combined with #860, we can derive the following theorem:

theorem sn_eta_steps_iff [DecidableEq Var] [HasFresh Var]   
(steps : t ↠ηᶠ t') : SN FullBeta t <-> SN FullBeta t'