case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝ : u ∈ support p
x u' : V
h : u ∈ support nil
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil nil u h)) ≤ 1

case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝ : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
h : u ∈ support (cons ha p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil (cons ha p') u h)) ≤ 1
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x : V
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p u h)) ≤ 1
induction' p with u' u' v' w' ha p' ih
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝¹ : u ∈ support p
x u' : V
h✝ : u ∈ support nil
h : u = u'
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil nil u h✝)) ≤ 1
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝ : u ∈ support p
x u' : V
h : u ∈ support nil
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil nil u h)) ≤ 1
rw [mem_support_nil_iff] at h
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' : V
h✝ : u' ∈ support p
h : u' ∈ support nil
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x)) (edges (takeUntil nil u' h)) ≤ 1
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝¹ : u ∈ support p
x u' : V
h✝ : u ∈ support nil
h : u = u'
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil nil u h✝)) ≤ 1
subst u
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' : V
h✝ : u' ∈ support p
h : u' ∈ support nil
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x)) (edges (takeUntil nil u' h)) ≤ 1
simp!
case cons.head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x v' w' : V
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
ha : Adj G u v'
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges (takeUntil (cons ha p') u (_ : List.Mem u (u :: support p')))) ≤
    1

case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges (takeUntil (cons ha p') u (_ : List.Mem u (u' :: support p')))) ≤
    1
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h✝ : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
h : u ∈ support (cons ha p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil (cons ha p') u h)) ≤ 1
cases h
no goals
case cons.head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x v' w' : V
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
ha : Adj G u v'
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges (takeUntil (cons ha p') u (_ : List.Mem u (u :: support p')))) ≤
    1
simp!
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges
        (if h : u' = u then
          Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
            (_ : List.Mem u (u' :: support p'))
        else cons ha (takeUntil p' u (_ : u ∈ support p')))) ≤
    1
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges (takeUntil (cons ha p') u (_ : List.Mem u (u' :: support p')))) ≤
    1
simp! only
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : u' = u
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
          (_ : List.Mem u (u' :: support p')))) ≤
    1

case cons.tail.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (cons ha (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges
        (if h : u' = u then
          Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
            (_ : List.Mem u (u' :: support p'))
        else cons ha (takeUntil p' u (_ : u ∈ support p')))) ≤
    1
split_ifs with h'
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
h : u' ∈ support p
ih : ∀ (h : u' ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x)) (edges (takeUntil p' u' h)) ≤ 1
a✝ : List.Mem u' (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x))
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u')
          (_ : List.Mem u' (u' :: support p')))) ≤
    1
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : u' = u
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x))
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
          (_ : List.Mem u (u' :: support p')))) ≤
    1
subst h'
no goals
case cons.tail.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w : V
p : Walk G v w
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
h : u' ∈ support p
ih : ∀ (h : u' ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x)) (edges (takeUntil p' u' h)) ≤ 1
a✝ : List.Mem u' (support p')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u', x))
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u')
          (_ : List.Mem u' (u' :: support p')))) ≤
    1
simp
case cons.tail.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ (if Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v') then
      Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p'))))
    else List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤
    1
case cons.tail.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (cons ha (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
rw [edges_cons, List.count_cons]
case cons.tail.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v')
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1

case cons.tail.inr.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p'))) ≤ 1
case cons.tail.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ (if Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v') then
      Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p'))))
    else List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤
    1
split_ifs with h''
case cons.tail.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : u = u' ∧ x = v' ∨ u = v' ∧ x = u'
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
case cons.tail.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v')
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
rw [Sym2.eq_iff] at h''
case cons.tail.inr.inl.inl.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x w' : V
h' : ¬u = u
p' : Walk G x w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
ha : Adj G u x
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1

case cons.tail.inr.inl.inr.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x w' : V
p' : Walk G u w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬x = u
ha : Adj G x u
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
case cons.tail.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : u = u' ∧ x = v' ∨ u = v' ∧ x = u'
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
no goals
case cons.tail.inr.inl.inl.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x w' : V
h' : ¬u = u
p' : Walk G x w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
ha : Adj G u x
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
exact (h' rfl).elim
no goals
case cons.tail.inr.inl.inr.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x w' : V
p' : Walk G u w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬x = u
ha : Adj G x u
⊢ Nat.succ (List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p')))) ≤ 1
cases p' <;> simp!
no goals
case cons.tail.inr.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x u' v' w' : V
ha : Adj G u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u h)) ≤ 1
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : ¬Quotient.mk (Sym2.Rel.setoid V) (u, x) = Quotient.mk (Sym2.Rel.setoid V) (u', v')
⊢ List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (edges (takeUntil p' u (_ : u ∈ support p'))) ≤ 1
apply ih