" 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