have := hs h
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
⊢ False
case mpr.intro.intro.intro.mk.intro.right
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
hd : (deleteEdges G' s).Adj v w = G'.Adj v w
this : (v, w) ∈ edgeSet G'
⊢ False