have : List.get? (List.reverse la' ++ [b]) la'.length = some b := by
  simpa using List.get?_concat_length la'.reverse b
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
case cons
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))