fix erroneous conclusion to penultimate lemma
bugfix in ReificationsIsomorphicToGeneralizedArrows
update to new coq-categories, base ND_Relation on inert sequences
remove unproven step1_lemma (it has a proof now)
lots of cleanup
reorganize flattening code
ReificationsIsomorphicToGeneralizedArrows: use EqDep
almost finished with main theorem
checkpoint
use WeakFunctorCategory to prove GArrow/Reification isomorphism