intro h
case mp
V : Type u_1
G G' : Digraph V
⊢ G < G' → ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s