Dependent Types + Combinatory Logic is highly non-trivial, as is shown in this series of work by Altenkirch et al.:

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.F...

https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...

https://types2023.webs.upv.es/slides/S22/TYPES2023-Altenkirc...

I wonder: Where does rholang3 fit in this?