Add (rather long and ugly) lemma about ap2-dep.
Show that (non-)dependent pairs preserve isSet.
Add Everything module to easily find out when something broke.