" u is a left factor of v "
Require Import Lists. Set Implicit Arguments. Inductive lfactor (A:Set) : list A -> list A -> Prop := lf1 : forall u:list A, lfactor nil u | lf2 : forall (a:A) (u v:list A), lfactor u v -> lfactor (a :: u) (a :: v).
Define a function meeting the following specification :
forall (A:Set) (u v:list A), lfactor u v -> {w : list A | v = u ++ w}.
Look at this file