proposition: Lemma size_trace lc : size (trace lc) = size lc.
proof: Proof. by case: lc => // *; rewrite /trace /ctrace /ptrace /= size_rcons size_pairmap. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)