add post condition on invariant
add postcodition on invariant of stream
adapt proof in WriteThenRead
adapt proofs in Encoder