Parallel le refl Trans Gen full Beta

lemma Parallel.le_reflTransGen_fullBeta :    ((· ⭢ₚ ·) : Term Var → Term Var → Prop) ≤ (· ↠βᶠ ·) := by  intro M N para  induction para  case fvar => constructor  case app L L' R R' l_para m_para redex_l redex_m =>    have : L.app R ↠βᶠ L'.app R := by grind    grind [ReflTransGen.trans]  case abs t t' xs _ ih =>    apply redex_abs_cong xs    grind  case beta m m' n n' xs para_ih para_n redex_ih redex_n =>    have m'_abs_lc : LC m'.abs := by      apply LC.abs xs      grind    calc      m.abs.app n ↠βᶠ      m'.abs.app n :=        redex_app_l_cong (redex_abs_cong xs (fun _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)      _           ↠βᶠ m'.abs.app n' := by grind      _           ⭢βᶠ m' ^ n'       := by grind