finish proof with admitted assertion
add .frama-c
move assertion to lemma