|
fe418c2a78
|
Fix preservation and broken cases in logrel
|
2025-03-03 15:29:50 -05:00 |
|
|
d68adf85f4
|
Finish refactoring substitution lemmas
|
2025-03-03 15:22:59 -05:00 |
|
Yiyun Liu
|
687d1be03f
|
Finish preservation
|
2025-02-25 22:35:59 -05:00 |
|
|
291d821d94
|
Add some admits to work on later
|
2025-02-25 16:12:44 -05:00 |
|
Yiyun Liu
|
48adb34946
|
Add simplified projection lemma
|
2025-02-12 19:53:20 -05:00 |
|
|
c1a8e9d2e1
|
Add the top-level subject reduction theorem
|
2025-02-10 21:51:27 -05:00 |
|
|
c5de86339f
|
Finish subject reduction
|
2025-02-10 21:50:23 -05:00 |
|