Changed equivalence relation formalization to just definitions and dependent refinement types. Changed the rest accordingly. Changes were to do refine_I, so streamlined.

Corrected quoed_codomain and refined_codomain statements to properly allow a predicate/bin. relation for every B x, instead just a single one. (Surprisingly, identical proofs work.)

Changed derivation of repeated quotient to pointwise check. Next: Documentation and chopping down into theories. Need to fix normal DHOL w/ subtypes on-the-fly.