no goals
f g h : ℕ →. ℕ
hf : Partrec f
hg : Partrec g
hh : Partrec h
a s : ℕ
⊢ (s ∈
      (Seq.seq (Nat.pair <$> Part.some a) fun x => f a) >>=
        unpaired fun a n =>
          Nat.rec (g a)
            (fun y IH => do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n) ↔
    s ∈
      Part.bind (f a) fun n =>
        Nat.rec (g a)
          (fun y IH => do
            let i ← IH
            h (Nat.pair a (Nat.pair y i)))
          n
simp [Seq.seq]