induction s using Finset.strongInduction generalizing G with
| _ s ih =>
  cases hs
  apply hind
  intros G' hG
  exact ih G'.edgeSet.toFinset (by simpa using hG) _ rfl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
G : Digraph V
this : Fintype V
s : Finset (V × V)
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
no goals