simp
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hbot : motive ⊥
hdelete : ∀ (G : Digraph V) (v w : V), ¬G.Adj v w → motive G → motive (G ⊔ ↑(OrderIso.symm (edgeSetIso V)) {(v, w)})
G : Digraph V
v w : V
hvw : G.Adj v w
ih : motive (deleteEdges G {(v, w)})
⊢ ¬(deleteEdges G {(v, w)}).Adj v w
no goals