Yannick Forster, Kathrin Stark: Coq à la carte: a practical approach to modular syntax with binders. CPP 2020: 186-200