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