fixing up the specification for type_cast_refl
complete proofs for SetoidRewrite

- need to fix the interface to support the new proofs
- still need to remove the intermediate type checking.
removing type check from setoid_rewrite.
changing setoid_rewrite to setoid_fold

- since it doesn't actually do rewriting.