theorem Std.Iterators.IterM.Equiv.forIn_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [IteratorLoop α₁ m n] [LawfulIteratorLoop α₁ m n] [IteratorLoop α₂ m n] [LawfulIteratorLoop α₂ m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ} {f : β → γ → n (ForInStep γ)} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : forIn ita init f = forIn itb init f

theorem Std.Iterators.IterM.Equiv.foldM_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α₁ m β] [Iterator α₂ m β] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [IteratorLoop α₁ m n] [LawfulIteratorLoop α₁ m n] [IteratorLoop α₂ m n] [LawfulIteratorLoop α₂ m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ} {f : γ → β → n γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : foldM f init ita = foldM f init itb

theorem Std.Iterators.IterM.Equiv.fold_eq {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Iterator α₁ m β] [Iterator α₂ m β] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [Monad m] [LawfulMonad m] [IteratorLoop α₁ m m] [LawfulIteratorLoop α₁ m m] [IteratorLoop α₂ m m] [LawfulIteratorLoop α₂ m m] {init : γ} {f : γ → β → γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : fold f init ita = fold f init itb

theorem Std.Iterators.IterM.Equiv.drain_eq {α₁ α₂ β : Type w} {m : Type w → Type w'} [Iterator α₁ m β] [Iterator α₂ m β] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [Monad m] [LawfulMonad m] [IteratorLoop α₁ m m] [LawfulIteratorLoop α₁ m m] [IteratorLoop α₂ m m] [LawfulIteratorLoop α₂ m m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : ita.drain = itb.drain