constructor
case insert.hs.a.mk
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 (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e ↔ (v, w) ∈ s
case insert.hs.a.mk.mp
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 (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e → (v, w) ∈ s

case insert.hs.a.mk.mpr
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 (deleteEdges G {(v, w)}) → motive G
this✝ : Fintype V
e : V × V
s : Finset (V × V)
he : ¬e ∈ s
ih : ∀ (G : Digraph V), Set.toFinset (edgeSet G) = s → motive G
G : Digraph V
this : e ∈ edgeSet G
v w : V
hs : G.Adj v w ↔ (v, w) = e ∨ (v, w) ∈ s
⊢ (v, w) ∈ s → ((v, w) = e ∨ (v, w) ∈ s) ∧ ¬(v, w) = e