The source code and proof output obtained for the source code found in section 5.2 Type Transformation of the paper "Software Refinement with Perfect Developer".
TypeTransformation.pd: A class that describes a type transformation of a set attribute with a sequence attribute