Lincx: A Linear Logical Framework With First-Class Contexts