Add notes about proving transformation correctness

These ideas may not make complete sense, but it's a start.