proposition: Lemma In_srs_stE {a b c d} : In ((a, b), (c, d)) srs -> ((sz, sz), (st, sr)) = ((a, b), (c, d)) \/ ((sz, st), (sl' 1, sm)) = ((a, b), (c, d)) \/ if a is (_, None) then (if b is (_, None) then False else True) else True.
proof: Proof. move=> /srs_specI [] [] > [] ? ? ? ? *; subst; by tauto. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun