proposition: Lemma eq2_app_app {u a b v u' v'} {s: list Symbol} : length s > 1 -> u ++ a :: b :: v = u' ++ s ++ v' -> (exists u'2, v = u'2 ++ s ++ v') \/ (exists s2, u' = u ++ [a] /\ s = b :: s2 /\ v = s2 ++ v') \/ (exists s1 s2, s = s1 ++ [a] ++ [b] ++ s2 /\ u = u' ++ s1 /\ v = s2 ++ v') \/ (exists s1, u = u' ++ s1 /\ s = s1 ++ [a] /\ v' = b :: v) \/ (exists v'1, u = u' ++ s ++ v'1).
proof: Proof. move=> Hs /eq2_app [|[|]]. - move=> [?] [-> ->]. left. by eexists. - move=> [->]. move: s Hs => [|? s] /=; first by lia. move=> _ [] <- <-. right. left. by eexists. - move=> [?] [->] /esym /eq2_app [|[|]]. + move=> [?] [-> ->]. right. right. left. by do 2 eexists. + move=> [-> ->]. do 3 right. left. by eexists. + move=> [?] [-> ->]. do 4 right. by eexists. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun