separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener.v, major improvements to flattening algorithm
remove many [[admit]]s from HaskProofFlattener.v
unbreak lots more stuff
fill in lots of missing proofs
update to new coq-categories, base ND_Relation on inert sequences
update to account for coq-categories changes
formatting fixes
reorganize flattening code