proposition: Lemma eptrace_inj lc f : injective f -> eptrace (map f lc) = eptrace lc.
proof: Proof. move=> injf; rewrite /eptrace -(ptrace_addc (f Color0)) -map_comp. have injf': injective (addc (f Color0) \o f) := inj_comp (addcI _) injf. have [|g /eq_map->] := color_inj_permc injf'; first by rewrite /= addcc. by rewrite ptrace_permt etail_permt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)