Removed level stuff from empty type. Created "isEmpty" function.
Added projection functions fst and snd for dependent pair.
Failed attempt at proving that qsAcc xs is in hProp.
Proved that for every x, y, x ≤ y is in hProp. Tried to write a makeIrrelevant function for hProp instead of only contractible types.