constructor <;> simp (config := { contextual := true }) [@h v w]
case Adj.h.h.a
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
H : Digraph V
h : H ≤ G
v w : V
⊢ (deleteEdges G (edgeSet G \ edgeSet H)).Adj v w ↔ H.Adj v w
no goals