Recursive name and nametype definitions

[zhengyao-lin]

Hello! As we discussed, I added support for recursive name and nametype definitions by (co)induction on the session index, and now a session index has an additional natural number like structure.

Examples:

name k<i>: enckey Name(k<succ(i)>)

nametype rec<i> = kdf {ikm info.
    info == 0x01 -> nonce,
    info == 0x02 -> strict kdf {
        info == 0x01 -> strict rec<succ(i)>
    }
}
name k: rec<0>

More examples can be found in tests/success/recursive_name.owl.
All current test cases are passing.

Some potential issues:

• I'm not sure about the change on subtyping. Previously names are fully unfolded in the subtyping check subNameType. I made it so that we don't unfold recursive name types initially in normalizeNameType, but instead unfold as needed when we actually comparing two types in subNameType. But I'm not completely sure if that interacts with other types well.
• No support for mutual recursion yet

Thanks in advance for any comments!