rintro ⟨s, _, rfl⟩
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'
case mpr.intro.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
left✝ : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'