System F in Agda using well-scoped de Bruijn indices

Terms, Types and Contexts are well-scoped.

References

• POPLMark: https://www.seas.upenn.edu/~plclub/poplmark/
• alan-j-hu/STLC: https://github.com/alan-j-hu/STLC
• sstucki/system-f-agda: https://github.com/sstucki/system-f-agda
• Jesper's 1001 Representations of Syntax with Binding: https://jesper.sikanda.be/posts/1001-syntax-representations.html
• Lysxia/system-F: https://github.com/Lysxia/system-F