proposition: Lemma fmap_app_inv l k1 k2 : f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
proof: Proof. revert l. induction k1 as [|y k1 IH]; simpl; [intros l ?; by eexists [],l|]. intros [|x l] ?; simplify_eq/=. destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2. Qed.
imports: stdpp(options)