no goals
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type ?u.40884
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ (Seq.seq (Nat.pair <$> Part.bind ↑(decode n) fun a => map encode (↑f a)) fun x =>
      Part.bind ↑(decode n) fun a => map encode (↑g a)) =
    Part.bind ↑(decode n) fun a => map encode ((↑fun a => (f a, g a)) a)
cases decode (α := α) n <;> simp [Seq.seq]