Move the flattening lemma to the core library, rename funext and happly, tidy up a few things