proposition: Lemma In_srsI {a b c d} : srs_spec a b c d \/ srs_mlr_spec a b c d -> In ((a, b), (c, d)) srs.
proof: Proof. case. - move=> [] > <- *. 1-2: apply /In_appl; rewrite /=; by tauto. 1-6: apply /In_appr /In_appl /in_flat_map; eexists; (constructor; [apply: instr_at_in_combine; by eassumption | by move=> /=; tauto ]). 1: apply /In_appr /In_appr /In_appr /In_appr /In_appl /in_map_iff; eexists; (constructor; [by reflexivity | apply /in_seq; by lia ]). 1-6: do 5 (apply /In_appr); move=> /=; subst; by tauto. - move=> [] p <- *. 1-7: apply /In_appr /In_appr /In_appl /in_flat_map; exists p; (constructor; [apply /in_seq; by lia | by move=> /=; tauto ]). 1-7: apply /In_appr /In_appr /In_appr /In_appl /in_flat_map; exists p; (constructor; [apply /in_seq; by lia | by move=> /=; tauto ]). Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun