adding a use of the record soundness proof.
adding an extra theorem about infinite types.