proposition: Lemma untrace_trace c0 lc : untrace c0 (trace (c0 :: lc)) = c0 :: lc.
proof: Proof. by rewrite /untrace /ctrace belast_rcons /= addc0 (pairmapK addKc). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)