proposition: Lemma in_split (A : eqType) (a : A) l : a \in l -> exists l1, exists l2, l = l1 ++ a :: l2.
proof: Proof. elim: l => //= b l IH; rewrite inE => /orP[/eqP<-|aIl]. by exists [::]; exists l. case: (IH aIl) => l1 [l2 lE]. by exists (b :: l1); exists l2; rewrite /= lE. Qed.
imports: mathcomp(all_ssreflect finmap)