{V : Type u} →
  {G : SimpleGraph V} →
    {u : V} →
      {p : G.Walk u u} →
        {motive : p.IsCycle → Sort u_1} →
          (t : p.IsCycle) → ((isCircuit : p.IsCircuit) → (support_nodup : p.support.tail.Nodup) → motive ⋯) → motive t