Add notion of isomorphism between OFEs

Add ofe_iso A B that states that OFEs A and B` are isomorphic. Some features:

• Proved that ofe_iso is reflexive, symmetric, and transitive. Note that I don't use the Equivalence class, since ofe_iso is a Type, not a Prop.
• Proved that ofe_iso A B itself is a OFE, and if A and B are COFEs, it's a COFE.
• Refactored the COFE solver to make use of ofe_iso.

I don't think it's extraordinarily useful that ofe_iso A B itself is a (C)OFE, but it holds, so why not have it :)