rwa [hs]
case empty
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), G.Adj v w → motive (deleteEdges G {(v, w)}) → motive G
this : Fintype V
G : Digraph V
hs✝ : Set.toFinset (edgeSet G) = ∅
hs : G = ⊥
⊢ motive G
no goals