proposition: Lemma app_n_1_app {T:Type} {n:nat} : forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))), app_n_1 pred cpp x -> allButLastCP cpt = cpp -> lastCP cpt = x -> app pred cpt.
proof: Proof. intros. induction n. simpl in *. rewrite H0; rewrite H1. apply H. apply IHn with (tailCP cpp); clear IHn. unfold app_n_1 in *. assert (H3 : (fst cpt) = fst (cpp)) by (rewrite <- H0; simpl; reflexivity). simpl in *. rewrite H3. apply H. rewrite <- H0. induction n. simpl; reflexivity. apply CP_ind. simpl; reflexivity. simpl in *; reflexivity. rewrite <- H1. induction n. simpl; reflexivity. simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality