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