I propose we add the GhostCell proof to the lambda-rust master. This is basically a cleanup and forward-port of the existing proof for that paper. The original proofs are by Joshua Yanovski.
The branch isn't done yet, I'll add more commits here as I make progress, but if you have comments already, feel free to chime in. :) I'll do my best to make the individual commits meaningful, so reviewing commit-by-commit is probably best.