Update Coq model to latest written rules.

Subtyping transitivity need to be rethought for rfn on the right,
because it uses loose expansion now.

Following 2949e35b429c86d3624e4dfcaf74ef7ee74d3d6b
          fbf9b49866dd9abc4a70e9d09b76f514369a7137