Bill's proof was based on proving a condition (actually, a sequence of conditions) that had previously been shown to suffice. One of the earliest known sufficient conditions was to derive an equation known has Huntington's axiom. See Bill's Web site for a full discussion.
To the best of our knowledge, presentations of the proof that Robbins algebras are Boolean have remained in the form of sequences of proofs, eventually leading to a proof of Huntington's equation. Here is a single Otter derivation of Huntington's axiom. Here is an Otter input file that can be used to check the derivation.