Add a proof of the Bourbaki-Witt fixpoint theorem.
Add copyright notices.
Add notations to ccl_scope.