proposition: Lemma app_n_1_app_eq {T:Type} {n:nat} : forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))), allButLastCP cpt = cpp -> lastCP cpt = x -> (app pred cpt <-> app_n_1 pred cpp x).
proof: Proof. intros. split. intro H1. apply (app_app_n_1 pred x cpp cpt H1 H H0). intro H1. apply (app_n_1_app pred x cpp cpt H1 H H0). Qed.
imports: Arith NArith List Sorting Coq.Program.Equality