∀ {α β : Type w} [inst : Std.Iterator α Id β] {a : Std.Iter β}
  {motive : (a_1 : Std.Iter β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop}
  {motive_1 :
    {a_1 : Std.Iter β} →
      (t : a.IsPlausibleIndirectSuccessorOf a_1) → Std.Iter.IsPlausibleIndirectSuccessorOf.below t → Prop}
  {a_1 : Std.Iter β} {t : a.IsPlausibleIndirectSuccessorOf a_1} (t_1 : Std.Iter.IsPlausibleIndirectSuccessorOf.below t),
  motive_1 ⋯ ⋯ →
    (∀ {it' it : Std.Iter β} (h' : a.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleSuccessorOf it)
        (ih : Std.Iter.IsPlausibleIndirectSuccessorOf.below h') (h'_ih : motive it' h'), motive_1 ⋯ ⋯) →
      motive_1 t t_1