Adding InliningproofEFF.v
Advancing the proof.
Little progress
Building the proof structure.
Progress
Trying to get in the repository
Progress
Two big subgoals left.
More progress on sepcomp proof
Make forward, especially forward_setx, slightly more efficient