(a b c : Card) : exp_card (b * c) a = exp_card c (exp_card b a). Proof. rewrite (@commutativity _ _ (.*.) _ b c). reduce. symmetry. apply equiv_uncurry. Defined.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.