∀ {n : Type u_1 → Type u_2} {α σ : Type u_1} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  [Std.Iterators.Finite σ n], WellFounded (InvImage Std.IterM.IsPlausibleSuccessorOf fun it => it.internalState.inner)