Fix sequence associativity
Compiler correctness proof