Some lemmas about eta-reduction and beta-eta equivalence

[binghe]

Hi,

This PR contains some new lemmas about lameta and reduction eta (-e->*) for solvable terms and hnfs. Most
important ones are the following two:

• Two βη-equivalent terms are either both solvable or both not:

[lameta_solvable_cong]
⊢ ∀M N. M === N ⇒ (solvable M ⇔ solvable N)

• The "cases" theorem for η-reductions from hnfs:

[hnf_etastar_cases]
⊢ ∀vs y Ms N.
    LAMl vs (VAR y ·· Ms) -η->* N ⇒
    ∃n Ns.
      N = LAMl (BUTLASTN n vs) (VAR y ·· BUTLASTN n Ns) ∧ n ≤ LENGTH vs ∧
      n ≤ LENGTH Ns ∧ LENGTH Ns = LENGTH Ms ∧
      LASTN n Ns = MAP VAR (LASTN n vs) ∧
      ∀i. i < LENGTH Ms ⇒ Ms❲i❳ -η->* Ns❲i❳

--Chun

[binghe]

Added also one more theorem (βη-reductions from hnf):

[hnf_bestar_cases]
⊢ ∀vs y Ms N.
    LAMl vs (VAR y ·· Ms) -βη->* N ⇒
    ∃n Ns.
      N = LAMl (BUTLASTN n vs) (VAR y ·· BUTLASTN n Ns) ∧ n ≤ LENGTH vs ∧
      n ≤ LENGTH Ns ∧ LENGTH Ns = LENGTH Ms ∧
      LASTN n Ns = MAP VAR (LASTN n vs) ∧
      ∀i. i < LENGTH Ms ⇒ Ms❲i❳ -βη->* Ns❲i❳