proposition: Lemma split_head (A : eqType) (a b : A) l1 l2 l3 l4 : l1 ++ a :: l2 = l3 ++ b :: l4 -> [\/ [/\ l1 = l3, a = b & l2 = l4], exists l5, l3 = l1 ++ a :: l5 | exists l5, l1 = l3 ++ b :: l5].
proof: Proof. elim: l1 l3 => /= [[[<- <-]|c l3 [<- ->]] /= | c l1 IH [[<- <-]|d l3 /= [<-]]]. - by apply: Or31. - by apply: Or32; exists l3. - by apply: Or33; exists l1. move=> /IH[[<- <- <-]|[l5 ->]|]. - by apply: Or31. - by apply: Or32; exists l5. by case=> l5 ->; apply: Or33; exists l5. Qed.
imports: mathcomp(all_ssreflect finmap)