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