cases hs
case H
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
s : Finset (V × V)
ih : ∀ (t : Finset (V × V)), t ⊂ s → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
G : Digraph V
hs : Set.toFinset (edgeSet G) = s
⊢ motive G
case H.refl
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
⊢ motive G