proposition: Lemma CPLRec {T : Type} : forall (a : T) l Default, (a :: (CPToList (ListToCP l Default))) = CPToList (ListToCP (a :: l) Default).
proof: Proof. intros a l Default. assert (HlAux := lengthOfCPToList (ListToCP l Default)). assert (Hl : S (length l) = length (a :: CPToList (ListToCP l Default))) by (simpl; apply eq_S; assumption); clear HlAux; apply eq_sym in Hl. assert (Hal := lengthOfCPToList (ListToCP (a :: l) Default)); apply eq_sym in Hal. apply listInd with (length l) Default; try assumption. rewrite CPLHd; simpl; reflexivity. assert (H : tl (a :: CPToList (ListToCP l Default)) = CPToList (ListToCP l Default)) by (simpl; reflexivity); rewrite H; clear H. induction l. simpl; reflexivity. clear IHl. assert (H := CPToListTl1 a a0 l (ListToCP (a :: a0 :: l) Default)); rewrite H; clear H. assert (H := CPCPL a0 l (ListToCP (a0 :: l) Default) (tailCP (ListToCP (a :: a0 :: l) Default))); apply H; clear H. assert (Ha0l : (S (length l)) = length (a0 :: l)) by (simpl; reflexivity). assert (Haa0l : (S (S (length l))) = length (a :: a0 :: l)) by (simpl; reflexivity). assert (H := ListToCPTl a a0 l Ha0l Haa0l Default); rewrite <- H; clear H. unfold tailCPbis. repeat (elim_eq_rect; simpl); reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality