proposition: Lemma trace_rcons c (lc : colseq) : trace (rcons lc c) = if trace (c :: lc) is e :: et then rcons et e else lc.
proof: Proof. case: lc => // c1 lc; rewrite rcons_cons !trace_cons /=. by elim: lc {1 3}c1 => //= c3 lc IHlc c2; rewrite IHlc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)