have : G.Adj v w → G'.Adj v w := fun e => h.le e
case mp.right.right.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)
case mp.right.right.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G < G'
v w : V
this : G.Adj v w → G'.Adj v w
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)