proposition: Lemma ListToCPTl {T : Type} : forall (a a0 : T) l (Ha0l : (S (length l)) = length (a0 :: l)) Haa0l Default, tailCPbis (length (a :: a0 :: l)) (length (a :: l)) (ListToCP (a :: a0 :: l) Default) Haa0l Ha0l = ListToCP (a0 :: l) Default.
proof: Proof. intros a a0 l Ha0l Haa0l Default. simpl in *. unfold tailCPbis. unfold tailCP. repeat (elim_eq_rect; simpl). induction l; simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality