simp only [deleteEdges_adj, Set.mem_diff, mem_edgeSet, not_and, not_not]
case mp.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
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)