ext p q
case h.e'_2
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e : V × V
⊢ instBEqProd = instBEq
case h.e'_2.beq.h.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
xs : List (V × V)
e p q : V × V
⊢ (p == q) = (p == q)