∀ {V : Type u_1} {G : SimpleGraph V} {v : V}
  (motive : (p : G.Walk v v) → p.IsCycle → p.IsTrail → p ≠ SimpleGraph.Walk.nil → p.support.tail.Nodup → Prop)
  (p : G.Walk v v) (hp : p.IsCycle) (hp_1 : p.IsTrail) (hp' : p ≠ SimpleGraph.Walk.nil)
  (support_nodup : p.support.tail.Nodup),
  (∀ (hp : SimpleGraph.Walk.nil.IsCycle) (hp_2 : SimpleGraph.Walk.nil.IsTrail)
      (hp' : SimpleGraph.Walk.nil ≠ SimpleGraph.Walk.nil) (support_nodup : SimpleGraph.Walk.nil.support.tail.Nodup),
      motive SimpleGraph.Walk.nil hp hp_2 hp' support_nodup) →
    (∀ (h : G.Adj v v) (hp : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).IsCycle)
        (hp_2 : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).IsTrail)
        (hp' : SimpleGraph.Walk.cons h SimpleGraph.Walk.nil ≠ SimpleGraph.Walk.nil)
        (support_nodup : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).support.tail.Nodup),
        motive (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) hp hp_2 hp' support_nodup) →
      (∀ (v_1 : V) (h : G.Adj v v_1) (h_3 : G.Adj v_1 v)
          (hp : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_3 SimpleGraph.Walk.nil)).IsCycle)
          (hp_2 : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_3 SimpleGraph.Walk.nil)).IsTrail)
          (hp' : SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_3 SimpleGraph.Walk.nil) ≠ SimpleGraph.Walk.nil)
          (support_nodup :
            (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_3 SimpleGraph.Walk.nil)).support.tail.Nodup),
          motive (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_3 SimpleGraph.Walk.nil)) hp hp_2 hp' support_nodup) →
        (∀ (v_1 : V) (h : G.Adj v v_1) (v_2 : V) (h_4 : G.Adj v_1 v_2) (v_3 : V) (h_5 : G.Adj v_2 v_3)
            (p : G.Walk v_3 v)
            (hp : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_4 (SimpleGraph.Walk.cons h_5 p))).IsCycle)
            (hp_2 : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_4 (SimpleGraph.Walk.cons h_5 p))).IsTrail)
            (hp' :
              SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_4 (SimpleGraph.Walk.cons h_5 p)) ≠ SimpleGraph.Walk.nil)
            (support_nodup :
              (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_4 (SimpleGraph.Walk.cons h_5 p))).support.tail.Nodup),
            motive (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h_4 (SimpleGraph.Walk.cons h_5 p))) hp hp_2 hp'
              support_nodup) →
          motive p hp hp_1 hp' support_nodup