add label Pre to assumes clauses
add {Pre} to assumes clauses of Encoder
add DecoderThenEncoder for Package_Foo
remove old proof
add rule for new file