proposition: Lemma ctrace_inj : injective ctrace.
proof: Proof. move=> et0 et0'; rewrite /ctrace; move: {-2}et0 {-2}et0'. by elim=> [|c et IHet] [|c' et'] //; [case et' | case et | case=> -> /IHet->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)