unfold intermediate definitions after sealing the bnf

bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned

tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD

more careful unfolding of internal constants

made typedef for the type of the bound optional (size-based)

made natLe{q,ss} constants (yields smaller terms in composition)

removed junk

tuned proofs;

unused;

tuned;