proposition: Lemma CPLOK {T : Type} : forall (l : list T) Default, CPToList (ListToCP l Default) = l.
proof: Proof. intros l Default. induction l. simpl; reflexivity. rewrite <- CPLRec. rewrite IHl. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality