have :
  mapM' (fun c => ((List.range ((s + 1).pair e)).map $ fun i => elimDecode β (f x) i.unpair.fst i.unpair.snd).getI (s.pair c))
    (Denumerable.ofNat (List ℕ) e.unpair.2) =
  mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2) :=
List.mapM'_eq_mapM'_of_eq _ (by
{ intro c hc
  have : s.pair c < (s + 1).pair e := by
    have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
    exact lt_of_lt_of_le (Nat.pair_lt_pair_right s this) (Nat.pair_le_pair_of_le (Nat.le_succ s) (Nat.unpair_right_le e))
  simp[List.getI_map_range _ this] })
case succ.e_a.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
case succ.e_a.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
σ : Type u_3
γ : Type u_4
f : σ → α → List γ → γ
x : σ
e s : ℕ
a : α
this :
  mapM'
      (fun c =>
        (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c))
      (Denumerable.ofNat (List ℕ) e.unpair.2) =
    mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)