Rel Triple list foldl M

lemma relTriple_list_foldlM    {σ₁ σ₂ : Type}    {xs : List α} {ys : List β}    {f : σ₁ → α → OracleComp spec₁ σ₁}    {g : σ₂ → β → OracleComp spec₂ σ₂}    {Rin : α → β → Prop} {S : σ₁ → σ₂ → Prop}    {s₁ : σ₁} {s₂ : σ₂}    (hs : S s₁ s₂)    (hxy : List.Forall₂ Rin xs ys)    (hfg : ∀ a b, Rin a b → ∀ t₁ t₂, S t₁ t₂ → RelTriple (f t₁ a) (g t₂ b) S) :    RelTriple (xs.foldlM f s₁) (ys.foldlM g s₂) S := by  induction hxy generalizing s₁ s₂ with  | nil =>    rw [List.foldlM_nil, List.foldlM_nil]    exact relTriple_pure_pure (R := S) (a := s₁) (b := s₂) hs  | @cons a b xs ys hab htl ih =>    rw [List.foldlM_cons, List.foldlM_cons]    exact relTriple_bind (hfg a b hab s₁ s₂ hs) fun t₁ t₂ ht => ih ht