proposition: Lemma match_etrace et w : matchg [::] (etrace et) w = matchg [::] et w.
proof: Proof. set sb := [::]; rewrite -{2}[sb]/(map negb sb) /etrace /etrace_perm. case (even_trace et); first by rewrite permt_id. elim: et sb w => [|e et IHet] lb [|s w] //; first by case lb. by case: e; case: s => //=; first [rewrite IHet | case: lb => [//|[]] /=]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)