proposition: Lemma srs_mlr_specE {a b c d} : srs_mlr_spec a b c d -> exists x y p, ((a, b), (c, d)) = (((x, Some p), (y, None)), ((x, None), (y, Some p))) \/ ((a, b), (c, d)) = (((x, None), (y, Some p)), ((x, Some p), (y, None))).
proof: Proof. move=> [] > [] ? ? ? ? _; subst; do 3 eexists; by tauto. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun