I've started proving some very simple language unambiguous, but I've gotten a bit stuck on natLang which is the language of natural numbers. The issue is that it uses a dependent sigma type, which is nontrivial to deal with.
Solving this issue is a requirement before we can move on to more complicated languages like #3
I've started proving some very simple language unambiguous, but I've gotten a bit stuck on
natLang
which is the language of natural numbers. The issue is that it uses a dependent sigma type, which is nontrivial to deal with.Solving this issue is a requirement before we can move on to more complicated languages like #3