proposition: Lemma app_1_n_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_1_n pred x cpp -> headCP cpt = x -> tailCP cpt = cpp -> app pred cpt.
proof: Proof. intros. induction n. simpl in *. rewrite H0; rewrite H1. apply H. clear IHn. simpl in *. rewrite H0; rewrite H1. apply H. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality