Library googology-in-coq のライブラリは Coq によりソースコードが書かれています。これらは Apache License 2.0 が適用されます。その範囲を厳密に言えば、このフォルダ内のファイル全てです。