constructor
case mp.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
case mp.right.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G'

case mp.right.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)