Some tweaks to ensure proofs still work with simple extensions.
Optional extension in comments. Proofs are the same.
Fix extension example.