proposition: Lemma trace_untrace c0 et : sumt et = Color0 -> trace (untrace c0 et) = et.
proof: Proof. case: et => // e1 et sum_et; rewrite /untrace /= /ptrace /= (scanlK addKc). rewrite /ctrace lastI -[last e1 et]add0c -{}sum_et; congr (rcons _ _). by elim: et e1 => [|e2 et IHet] e1 /=; rewrite -addcA ?addcc ?IHet. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)