proposition: Lemma CPLHd {T : Type} : forall (a : T) l Default, hd Default (CPToList (ListToCP (a :: l) Default)) = a.
proof: Proof. intros a l Default. induction l. simpl; reflexivity. simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality