proposition: Lemma trace_cons c lc : trace (c :: lc) = pairmap addc c (rcons lc c).
proof: Proof. rewrite /trace /ptrace /ctrace /= -[sumt _](addKc c). elim: lc {-2 6}c => [|c2 lc IHlc] c1 /=; first by rewrite addc0 addcC. by rewrite -!addcA addKc IHlc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)