proposition: Lemma split_tail (A : eqType) (a b : A) l1 l2 l3 l4 : l1 ++ a :: l2 = l3 ++ b :: l4 -> [\/ [/\ l1 = l3, a = b & l2 = l4], exists l5, l4 = l5 ++ a :: l2 | exists l5, l2 = l5 ++ b :: l4].
proof: Proof. elim/last_ind : l2 l4 => [l4|l2 c IH l4]. case: (lastP l4) => /= [|l5 c]. rewrite !cats1 => /rcons_inj[<- <-]. by apply: Or31. rewrite cats1 -rcons_cons -rcons_cat => /rcons_inj[-> <-]. by apply: Or32; exists l5; rewrite cats1. case: (lastP l4) => /= [|l5 d]. rewrite cats1 -rcons_cons -rcons_cat => /rcons_inj[<- ->]. by apply: Or33; exists l2; rewrite cats1. rewrite -!rcons_cons -!rcons_cat => /rcons_inj[/IH [[<- <- <-]|[l6 ->]|[l6 ->]]] <-. - by apply: Or31. - by apply: Or32; exists l6; rewrite -rcons_cat. by apply: Or33; exists l6; rewrite -rcons_cat. Qed.
imports: mathcomp(all_ssreflect finmap)