This paper gives a new presentation of Kozen's proof of Kleene algebra completeness featured in his article "A completeness theorem for Kleene algebras and the algebra of regular events". A few new variants are introduced, shortening the proof. Specifically, we directly construct an epsilon-free automaton to prove an equivalent to Kleene's representation theorem (implementing Glushkov's instead of Thompson's construction), and we bypass the use of minimal automata by directly implementing a Myhill-Nerode equivalence relation on the union of equivalent deterministic automata.