proposition: Lemma trace_permt g lc : trace (permt g lc) = permt g (trace lc).
proof: Proof. by case: lc => // c lc; rewrite /trace -ctrace_permt -ptrace_permt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)