Renaming F?

[andres-erbsen]

Тhe F type is quite central to fiat-crypto, but it's naming is unwise considering the full range of arguments it could be instantiated with. Currently we have only been using prime moduli, but nothing prevents the same definition from being instantiated with a composite, and I can think of on instance where I say a probably-mistaken F (2^k) with fiat-crypto F. As is, this instantiation defines the integers modulo 2^k, which is a ring but not a field. As we're now considering adding actual formalization of extension fields, it might be time to figure out another name for F. (I figure having type-level computation that factors the argument is beyond our dependently-typed-programming ambitions).