What you're calling a dynamic type is what he'd call a canonical form. If your typing system has product types, then you should be able to prove that anything with a product type evaluates down to an ordered pair.