rw [edgeSetIso_symm_adj]
case h.e'_1.Adj.h.h.a
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)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (↑(OrderIso.symm (edgeSetIso V)) {(v, w)}).Adj a b
case h.e'_1.Adj.h.h.a
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)})
a b : V
⊢ G.Adj a b ↔ G.Adj a b ∧ (a = v → ¬b = w) ∨ (a, b) ∈ {(v, w)}