constructor
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' ↔ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
case mp
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' → ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s

case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'