proposition: Lemma stepI {srs u v a b c d s t} : s = (u ++ a :: b :: v) -> t = (u ++ c :: d :: v) -> In ((a, b), (c, d)) srs -> step srs s t.
proof: Proof. move=> -> ->. by constructor. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun