proposition: Lemma srs_specI a b c d : In ((a, b), (c, d)) srs -> srs_spec a b c d \/ srs_mlr_spec a b c d.
proof: Proof. rewrite /srs. case /in_app_iff. { firstorder (by eauto using srs_spec with nocore). } case /in_app_iff. { move=> /in_flat_map [[? i]] [/inv_instr_at_in_combine]. move: i => []> /=; intuition (by eauto using srs_spec, or with nocore). } case /in_app_iff. { move=> /in_flat_map [?] [/in_seq] [_ ?]. firstorder (by eauto using srs_mlr_spec with nocore). } case /in_app_iff. { move=> /in_flat_map [?] [/in_seq] [_ ?]. firstorder (by eauto using srs_mlr_spec with nocore). } case /in_app_iff. { move=> /in_map_iff [?] [?] /in_seq H. left. apply: srs_fin0; first by eassumption. move: H. rewrite /state_bound. by lia. } case. { move=> [] *. subst. left. by eauto using srs_spec, erefl with nocore. } by firstorder (by eauto using srs_spec with nocore). Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun