(* EXO mots *)
Section MOTS.

Variable char : Set.
Variable a : char.
Variable b : char.

Require Import List.
Definition word : Set := list char.

Definition pempty (w:word) : Prop := (w = nil).
Definition pchar (c:char) (w:word) : Prop := (w = c::nil).

Definition pconcat (p1:word -> Prop) (p2:word -> Prop) (w : word):= (* ... *)

Theorem pconcat_empty : forall p w, pconcat p pempty w -> p w.
Proof.
(* ... *)
Qed.

Inductive pstar (p:word -> Prop) : word -> Prop := 
(* ... *)

Theorem star_concat :
  forall (p:word->Prop) w1 w2,  p w1 -> pstar p w2 -> pstar p (app w1 w2).
Proof.
(* ... *)
Qed.

Theorem concat_star :
  forall (p:word->Prop) w1 w2,  pstar p w1 -> p w2 -> pstar p (app w1 w2).
Proof.
(* ... *)
Qed.

Theorem star_pconcat : 
  forall (p:word->Prop) w, pconcat (pstar p) p w -> pstar p w.
(* ... *)
Qed.

End MOTS.