proposition: Lemma fixLastCPOK {T:Type} {n:nat} : forall (appPred : cartesianPower T (S (S n)) -> Prop) (cp : cartesianPower T (S n)) (t : T), appPred (consTailCP cp t) = (fixLastCP appPred t) cp.
proof: Proof. intros appPred cp; unfold fixLastCP; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality