proposition: Lemma pcaHdTl {T:Type} {n:nat} : forall (pred : arity T (S n)) m cp cpwd, pred_conj_aux pred (S m) cp cpwd = (app_1_n pred (headCP cp) cpwd /\ pred_conj_aux pred m (tailCP cp) cpwd).
proof: Proof. unfold pred_conj_aux; unfold nat_rect; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality