proposition: Corollary genColor_correctSize': forall s, semProdSize genColor s <--> setT.
proof: Proof. move => s. rewrite unsized_alt_def. by apply semColor. Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype) List String Lia QuickChick(QuickChick) QuickChick.RedBlack(redblack testing)