proposition: Lemma eq2_app {u v a b} {s t: list Symbol} : u ++ a :: b :: v = s ++ t -> (exists v1, v = v1 ++ t /\ s = u ++ a :: b :: v1) \/ (s = u ++ [a] /\ t = b :: v) \/ (exists u2, u = s ++ u2 /\ t = u2 ++ a :: b :: v).
proof: Proof. elim: u s. - move=> [|y1 [|y2 s]]. + rewrite ?app_nil_l. move=> <-. right. right. by exists []. + move=> [] <- <- /=. right. by left. + move=> [] <- <- ->. left. by exists s. - move=> x1 u IH [|y1 s]. + rewrite ?app_nil_l. move=> <-. right. right. by exists (x1 :: u). + move=> [] <- /IH [|[|]]. * move=> [?] [-> ->]. left. by eexists. * move=> [-> ->]. right. by left. * move=> [?] [-> ->]. right. right. by eexists. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun