Embed Notice

I think this can be extended from affine to linear theories, now you need to take more seriously that this thing is bidirectional, by which I mean "yet another thing that's secretly a dependent affine traversal". When you pass through a lambda you add its variable(s) to your context, but then when you've finished checking the lambda's subterm you pass backwards up through the lambda again, at which point the lambda checks that all the variables it added are no longer there, and fails with a quantity error if any are