Completed outer proof structure, added lots of sorries, cleaned up a bit, deleted old proof structure.