I really appreciate the proof of Arrow’s impossibility theorem that you’ve included in this course. It’s a very elegant and satisfying proof of a surprisingly powerful result.
However, I believe I have spotted a minor error in your formulation of the contraction lemma. As stated, the lemma is trivial because the empty set is always a proper subset of any set with at least two members and the empty set is also trivially decisive over any two alternatives. For the lemma to do what you need it to, it has to conclude that the decisive proper subset of G is non-empty (and you already show non-emptiness in the proof).