make Op' not depend on funext
Merge branch 'localization' into modules

Conflicts:
	theories/hit/PropositionalFracture.v