doc: update information on licenses

Currently, this repository has two licenses.

README.ko.md

@@ -2,7 +2,9 @@
 
 [English (영어)](./README.md) | 한국어
 
-[제러미 아비가드][ja], [레오나르두 지 모라][ldm], [공순호][sk], [제바스티안 울리히][su] 님이 저술하고, [린 커뮤니티][lean-comm]의 기여를 받아 개정된 ["린 4로 하는 정리 증명"][tpil]의 제 연습 문제 풀이가 이 저장소에 들어 있습니다. 이 저작물은 [아파치 라이선스, 버전 2.0](./LICENSE)의 조건에 따라 재이용할 수 있습니다.
+[제러미 아비가드][ja] 님, [레오나르두 지 모라][ldm] 님, [공순호][sk] 님 그리고 [제바스티안 울리히][su] 님이 저술하고, [린 커뮤니티][lean-comm]의 기여를 받아 개정된 ["린 4로 하는 정리 증명"][tpil]의 제 연습 문제 풀이가 이 저장소에 들어 있습니다.
+
+이 저작물의 대부분은 [아파치 라이선스, 버전 2.0](./LICENSE)의 조건에 따라 배포됐습니다. 그러나 이 저장소에는 [자유 이용 저작물](./LICENSE-CC0)인 린 파일도 있습니다.
 
 교재 각 장의 퀴즈와 제 풀이도 이 저장소에 포함했습니다.
 

README.md

@@ -5,8 +5,11 @@ English | [한국어[Korean]](./README.ko.md)
 This is the repository for my solutions to the exercises in ["Theorem Proving in
 Lean 4"][tpil] by [Jeremy Avigad][ja], [Leonardo de Moura][ldm], [Soonho
 Kong][sk] and [Sebastian Ullrich][su], with contributions from the [Lean
-Community][lean-comm]. You are free to reuse the content under the terms of
-[Apache License Version 2.0](./LICENSE).
+Community][lean-comm].
+
+Most of the content has been released under the terms of [Apache License Version
+2.0](./LICENSE). However, this repository also contains a Lean file in the
+[public domain](./LICENSE-CC0).
 
 I've also included a quiz for each chapter of the text in this repository, along
 with my solutions to the questions in each quiz.

docs/ko/README.md

@@ -2,7 +2,9 @@
 
 [English (영어)](./README.md) | 한국어
 
-[제러미 아비가드][ja], [레오나르두 지 모라][ldm], [공순호][sk], [제바스티안 울리히][su] 님이 저술하고, [린 커뮤니티][lean-comm]의 기여를 받아 개정된 ["린 4로 하는 정리 증명"][tpil]의 제 연습 문제 풀이가 이 저장소에 들어 있습니다. 이 저작물은 [아파치 라이선스, 버전 2.0](./LICENSE)의 조건에 따라 재이용할 수 있습니다.
+[제러미 아비가드][ja] 님, [레오나르두 지 모라][ldm] 님, [공순호][sk] 님 그리고 [제바스티안 울리히][su] 님이 저술하고, [린 커뮤니티][lean-comm]의 기여를 받아 개정된 ["린 4로 하는 정리 증명"][tpil]의 제 연습 문제 풀이가 이 저장소에 들어 있습니다.
+
+이 저작물의 대부분은 [아파치 라이선스, 버전 2.0](./LICENSE)의 조건에 따라 배포됐습니다. 그러나 이 저장소에는 [자유 이용 저작물](./LICENSE-CC0)인 린 파일도 있습니다.
 
 교재 각 장의 퀴즈와 제 풀이도 이 저장소에 포함했습니다.
 

docs/omegat/project_save.tmx

@@ -1136,6 +1136,15 @@ prover as follows:</seg>
         <seg>그러나 (2)가 명제인지를 둘러싸고 두 분의 의견이 갈렸습니다.</seg>
       </tuv>
     </tu>
+    <tu>
+      <tuv lang="en">
+        <seg>However, this repository also contains a Lean file in the
+&lt;g2&gt;public domain&lt;/g2&gt;.</seg>
+      </tuv>
+      <tuv lang="ko" changeid="chabulhwi" changedate="20250102T150054Z" creationid="chabulhwi" creationdate="20250102T150011Z">
+        <seg>그러나 이 저장소에는 &lt;g2&gt;자유 이용 저작물&lt;/g2&gt;인 린 파일도 있습니다.</seg>
+      </tuv>
+    </tu>
     <tu>
       <tuv lang="en">
         <seg>I don't think the usage of the term 'proposition' in Korean high school
@@ -1469,6 +1478,15 @@ where &lt;g6&gt;p x&lt;/g6&gt; holds."</seg>
         <seg>뜻: 유형 &lt;g1&gt;α&lt;/g1&gt;와 단항 술어 &lt;g2&gt;p : α → Prop&lt;/g2&gt;가 주어져 있을 때, 명제 &lt;g3&gt;∃ (x : α), p x&lt;/g3&gt;는 "유형 &lt;g5&gt;α&lt;/g5&gt;에 속하고 &lt;g6&gt;p x&lt;/g6&gt;를 성립시키는 항 &lt;g4&gt;x&lt;/g4&gt;가 존재한다."라는 뜻이다.</seg>
       </tuv>
     </tu>
+    <tu>
+      <tuv lang="en">
+        <seg>Most of the content has been released under the terms of &lt;g1&gt;Apache License Version
+2.0&lt;/g1&gt;.</seg>
+      </tuv>
+      <tuv lang="ko" changeid="chabulhwi" changedate="20250102T150000Z" creationid="chabulhwi" creationdate="20250102T150000Z">
+        <seg>이 저작물의 대부분은 &lt;g1&gt;아파치 라이선스, 버전 2.0&lt;/g1&gt;의 조건에 따라 배포됐습니다.</seg>
+      </tuv>
+    </tu>
     <tu>
       <tuv lang="en">
         <seg>My Closing Thoughts</seg>
@@ -2275,6 +2293,17 @@ text.</seg>
     <tu>
       <tuv lang="en">
         <seg>This is the repository for my solutions to the exercises in &lt;g1&gt;"Theorem Proving in
+Lean 4"&lt;/g1&gt;&lt;g2&gt;&lt;/g2&gt;&lt;e13/&gt; by &lt;g3&gt;Jeremy Avigad&lt;/g3&gt;&lt;g4&gt;&lt;/g4&gt;&lt;e14/&gt;, &lt;g5&gt;Leonardo de Moura&lt;/g5&gt;&lt;g6&gt;&lt;/g6&gt;&lt;e15/&gt;, &lt;g7&gt;Soonho
+Kong&lt;/g7&gt;&lt;g8&gt;&lt;/g8&gt;&lt;e16/&gt; and &lt;g9&gt;Sebastian Ullrich&lt;/g9&gt;&lt;g10&gt;&lt;/g10&gt;&lt;e17/&gt;, with contributions from the &lt;g11&gt;Lean
+Community&lt;/g11&gt;&lt;g12&gt;&lt;/g12&gt;&lt;e18/&gt;.</seg>
+      </tuv>
+      <tuv lang="ko" changeid="chabulhwi" changedate="20250102T150833Z" creationid="chabulhwi" creationdate="20250102T145847Z">
+        <seg>&lt;g3&gt;제러미 아비가드&lt;/g3&gt;&lt;g4&gt;&lt;/g4&gt;&lt;e14/&gt; 님, &lt;g5&gt;레오나르두 지 모라&lt;/g5&gt;&lt;g6&gt;&lt;/g6&gt;&lt;e15/&gt; 님, &lt;g7&gt;공순호&lt;/g7&gt;&lt;g8&gt;&lt;/g8&gt;&lt;e16/&gt; 님 그리고 &lt;g9&gt;제바스티안 울리히&lt;/g9&gt;&lt;g10&gt;&lt;/g10&gt;&lt;e17/&gt; 님이 저술하고, &lt;g11&gt;린 커뮤니티&lt;/g11&gt;&lt;g12&gt;&lt;/g12&gt;&lt;e18/&gt;의 기여를 받아 개정된 &lt;g1&gt;"린 4로 하는 정리 증명"&lt;/g1&gt;&lt;g2&gt;&lt;/g2&gt;&lt;e13/&gt;의 제 연습 문제 풀이가 이 저장소에 들어 있습니다.</seg>
+      </tuv>
+    </tu>
+    <tu>
+      <tuv lang="en">
+        <seg>This is the repository for my solutions to the exercises in &lt;g1&gt;"Theorem Proving in
 Lean 4"&lt;/g1&gt;&lt;g2&gt;&lt;/g2&gt;&lt;e14/&gt; by &lt;g3&gt;Jeremy Avigad&lt;/g3&gt;&lt;g4&gt;&lt;/g4&gt;&lt;e15/&gt;, &lt;g5&gt;Leonardo de Moura&lt;/g5&gt;&lt;g6&gt;&lt;/g6&gt;&lt;e16/&gt;, &lt;g7&gt;Soonho
 Kong&lt;/g7&gt;&lt;g8&gt;&lt;/g8&gt;&lt;e17/&gt; and &lt;g9&gt;Sebastian Ullrich&lt;/g9&gt;&lt;g10&gt;&lt;/g10&gt;&lt;e18/&gt;, with contributions from the &lt;g11&gt;Lean
 Community&lt;/g11&gt;&lt;g12&gt;&lt;/g12&gt;&lt;e19/&gt;.</seg>