WIP: alternative proof of strong normalization, following Lemma 3.2.1 - #21

Draft

j-bmn wants to merge 8 commits into

bwerner:mainfrom

j-bmn:strong-normalization-variant

Commits on Dec 10, 2024

WIP: alternative proof of strong normalization, following Lemma 3.2.1
j-bmn
committed
e842635
WIP: proper proof structure for base case of Lemma 3.2.1
j-bmn
committed
5a3ee77
WIP: resolve some simple subgoals
j-bmn
committed
e944a1b
WIP: more progress on base case of 3.2.1
j-bmn
committed
355bf7c
WIP: resolve one more admitted goal
j-bmn
committed
0026516
WIP: resolve more admitted cases
j-bmn
committed
c6a0460
Prove remaining case.
j-bmn
committed
ee0c0cf
reduce dependency on auto-generated names
j-bmn
committed
7ba5d9c