ext a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ↑(direct_succ_list g x).toFinset = direct_succ_set g x
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ direct_succ_set g x