generalize hs : G.edgeSet.toFinset = s
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
⊢ motive G
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