proposition: Lemma InCPOK {T:Type} {n:nat} : forall p (cp : cartesianPower T (S (S n))), InCP p cp <-> ((p = headCP cp) \/ InCP p (tailCP cp)).
proof: Proof. intros p cp; unfold InCP; induction n; simpl. split; intro H. elim H; clear H; intro H. left; subst; reflexivity. right; assumption. elim H; clear H; intro H. left; subst; reflexivity. right; assumption. split; intro H. elim H; clear H; intro H. left; subst; reflexivity. right; assumption. elim H; clear H; intro H. left; subst; reflexivity. right; assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality