∀ {V : Type u_1} (G : SimpleGraph V) (n : ℕ),
  let s := {n | ∃ u v p, p.IsTrail ∧ p.length = n};
  ∀ (motive : n ∈ s → Prop) (x : n ∈ s),
    (∀ (w w_1 : V) (w_2 : G.Walk w w_1) (hp : w_2.IsTrail) (hn : w_2.length = n), motive ⋯) → motive x