proposition: Lemma In_srsI u v : In (u, v) srs -> In_srs u v.
proof: Proof. move=> /in_flat_map [[q a]] [_] /=. case E: (trans' M (q, a)) => [[[q' a'] []]|] /=. - move=> [|[|[|[]]]] => - [<- <-]. all: by auto using In_srs_l1, (In_srs_l2 _ true), (In_srs_l2 _ false). - move=> [|[|[|[]]]] => - [<- <-]. all: by auto using In_srs_r1, (In_srs_r2 _ true), (In_srs_r2 _ false). - move=> [|[|[|[|[|[]]]]]] => - [<- <-]. all: by auto using In_srs_f, (In_srs_dl _ true), (In_srs_dl _ false), (In_srs_dr _ true), (In_srs_dr _ false). Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun