∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] {ita itb itc : Std.BundledIterM m β},
  Std.BundledIterM.Equiv m β ita itb → Std.BundledIterM.Equiv m β itb itc → Std.BundledIterM.Equiv m β ita itc