apply dom_bool₂.comp₂ (hp.comp₂ (fst.comp₂ $ fst.comp₂ .left) .right) (snd.comp₂ $ snd.comp₂ .left)
α✝ : 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
⊢ Computable₂ fun p_1 val => (fun b => p p_1.1.1 b && p_1.2.2) val
no goals