proposition: Lemma In_srsE u v : In_srs u v -> In (u, v) srs.
proof: Proof. case=> q a > E => [|[]|[]||[]||[]]. all: have ? : In a [true; false] by (case: (a) => /=; tauto). all: have ? := all_fins_spec q. all: apply /in_flat_map; exists (q, a). all: split; first by apply: in_prod. all: by rewrite /= E /=; tauto. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun