reorder some unfolds
save state
finish proof with admitted assertion
add .frama-c
move assertion to lemma