`listFullBeta_cons_r` should rename to `listFullBeta_concat_r`

[lengyijun]

As well as listFullBeta_cons_l

lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by
  induction h with grind