Begins work on #671 (closed)
Modifies some proofs in Alpha_context.v and Raw_context.v
Alpha_context.v
Raw_context.v