proposition: Lemma app_app_2_n_default {T:Type} {n:nat} : forall (pred : arity T (S (S n))) (x1 x2 : T) (cpp Default : cartesianPower T n) (cpt : cartesianPower T (S (S n))), app pred cpt -> headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailDefaultCP (tailCP cpt) Default = cpp -> app_2_n pred x1 x2 cpp.
proof: Proof. intros. induction n. simpl in *. rewrite <- H0; rewrite <- H1; rewrite <- H2. apply H. clear IHn. simpl in *. rewrite <- H0; rewrite <- H1; rewrite <- H2. apply H. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality