ยง Proof of tree having (V-1) edges

I'm more comfortable with the proof where we link the vertex to the incoming edge "all at once". The proof of induction feels weird. So sahiti suggested: impose an ordering that makes the time feel better. So if I imagine the tree losing leaves from the bottom up left to right, it feels a lot smoother. So sahiti also suggested: shake the tree! This feels better as well. In general, I think I prefer thinking of it in terms of "applicative", instead of "monad, where the choices are statically determined, and I am not forced to make an arbitrary choice at each step, since the arbitrariness of the choice breaks my "flow".