jnkrtech on Nostr: nprofile1q…d6kk0 nprofile1q…ulpgt That does, thank you! I was trying to store the ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt (nprofile…lpgt) That does, thank you! I was trying to store the indices as ints rather than as an inductive type. Does this indexing make it easier to write proofs about the systems? Or is it to maintain correctness when writing substitution etc operations?