forall P : Operations -> Type, P A -> P B. Proof. intros P;apply transport. first [exact iso_same_semirings|exact iso_same_semirings@{V V}]. Qed.
Require Import Require Import HoTT.Classes.theory.rings.