proposition: Lemma rewrite_path_sym x y : (forall x y, x \in rule y -> y \in rule x) -> rewrite_path x y -> rewrite_path y x.
proof: Proof. Proof using. move=> Hsym [pathxy]; rewrite -rev_path => Hxy Hy. move: Hxy; rewrite -Hy. case/lastP: pathxy Hy => [/= -> _ | pathxz z]; first exact: (Rew [::]). rewrite last_rcons belast_rcons rev_cons => ->{y} Hpath. apply: (Rew (rcons (rev pathxz) x)). - set rel := (X in path X _ _) in Hpath. rewrite (eq_path (e' := rel)); first exact: Hpath. by move=> i j; rewrite /rel; apply/idP/idP; exact: Hsym. - by rewrite last_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK