proposition: Lemma sumt_ctrace et : sumt (ctrace et) = Color0.
proof: Proof. rewrite /ctrace -(add0c (sumt et)). elim: et Color0 => [|e et IHet] c /=; first by rewrite 2!addc0. by rewrite addcA IHet (addcC c e) addKc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)