Distributive property with sum types and product types
Polynomial types (those obtained through $+,\times,0,1$ and type variables) form a commutative semiring. 

Basically, all the elementary arithmetic laws for $+$ and $\times$ hold as expected, up to (natural) isomorphism. These include commutativity, associativity, and distributivity of $\times$ over $+$.

More concretely, the distributive law is
$$ (A\times C)+(B\times C) \simeq (A+B)\times C$$
and I think this was the law that Philip Wadler meant to show.