proposition: Lemma consHdInterpOK : forall (cp : cartesianPower positive 1) (x : tST) interp, consHeadCP (interp_CP cp interp) (interp_CP x interp) = interp_CP (consHeadCP cp x) interp.
proof: Proof. intros cp x interp. apply CP_ind; simpl; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets