About Left Factors

" 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).

 forall (A:Set) (u v:list A), lfactor u v -> {w : list A | v = u ++ w}.

Solution