proposition: Lemma app_2_n_app_eq {T:Type} {n:nat} : forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))), headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailCP (tailCP cpt) = cpp -> (app pred cpt <-> app_2_n pred x1 x2 cpp).
proof: Proof. intros. split. intro H2. apply (app_app_2_n pred x1 x2 cpp cpt H2 H H0 H1). intro H2. apply (app_2_n_app pred x1 x2 cpp cpt H2 H H0 H1). Qed.
imports: Arith NArith List Sorting Coq.Program.Equality