Ci.v: initial commit

Proofs related to serial merge processes.