proposition: Lemma ptrace_permt g lc : ptrace (permt g lc) = permt g (ptrace lc).
proof: Proof. rewrite /ptrace; case: lc => //= c lc; elim: lc c => //= c' lc IHlc c. by rewrite IHlc permc_addc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)