refactor(Mathlib/Data/Seq/Seq): make `Seq'.mem_rec_on` more useful

[Komyyy]

theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
    (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s

to

theorem mem_rec_on {a} {C : (s : Seq' α) → a ∈ s → Prop} {s} (M : a ∈ s)
    (mem_cons : ∀ s, C (cons a s) (mem_cons a s))
    (mem_cons_of_mem : ∀ (y) {s} (h : a ∈ s), C s h → C (cons y s) (mem_cons_of_mem y h)) :
    C s M

This change make Seq'.mem_rec_on available in induction tactic.

---

• [ ] depends on: #13361

This PR consists Continued fractions makes an isomorphism between irrationals and baire space project