In this paper, we represent in type theory
a proof system for refinement of algebraic specifications. .
The representation is not adequate but full because the
use of proof obligations to represent side-conditions.
Using this representation, we
can develop a proof tactic to help the development of proofs
Mylonakis, N. "Proof assistance for refnement in type theory". 2003.