proposition: Lemma rew_swap {X} {R : SR.SRS X} {x y} : SR.rew (map SR.swap R) x y -> SR.rew R y x.
proof: Proof. move ER': (map _ _) => R' H. case: H ER' => > + ?. subst R'. by move=> /in_map_iff [[??]] [[]] <- <- /SR.rewB. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun