proposition: Lemma etail_permt g et : etail (permt g et) = etail et.
proof: Proof. case et_ok: (proper_trace et); last first. by rewrite /etail /ttail proper_permt et_ok /= 2!permc0. have get_ok: proper_trace (permt g et) by rewrite proper_permt. have{et_ok get_ok} [[h Dhet] [h']] := (etail_perm et_ok, etail_perm get_ok). have [g' <-{h'} Dg'et] := compose_permt h' g et. have [g'' Eg''] := compose_permt g' (inv_eperm h) (permt h et). rewrite {4}/permt (mapK (inv_permc h)) {g'}Dg'et {h}Dhet /= in Eg''. case: Eg'' (even_etail et) (even_etail (permt g et)) => g''1 <-. case: g'' g''1 => // _; first by rewrite permt_id. by elim: {et}(etail et) => [|[] et IHet] //= *; rewrite IHet. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)