cases term_eq₁
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₁ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₁ : τ G edge = τ₁
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := term_eq₁ }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }