fixed predicative universes to obey actual subtyping relation
increased hardness of impredicitivity check
fixed predicative universes broke zippers
added some examples