ext v w
case mp.right.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w