Stan Wagon's exposition of Banach-Tarski (for example) includes a beautiful explicit construction of two 2-sphere rotations which generate a free subgroup of the rotation group.

For teaching purposes I'd like the fastest, quick and dirty soft proof.

A further thought or two:

Presumably, given a nontrivial word in the free group on two generators, only a "small" set of pairs of rotations satisfy the word. Small could mean measure zero or nowhere dense. But I don't see an easy proof of this.

Some words such as $aba^{-1}b^{-1}$ have infinitely many solutions even once you choose a rotation to substitute for $a$ (all the rotations with the same axis will work for $b$). But I'd guess that such words are atypical - that usually fixing $a$ would reduce your choices for $b$ to a set of dimension $0$. What is the right theorem?