proposition: Lemma interp_CPHdOK {m : nat} : forall (cp : cartesianPower positive (S m)) interp, interp_CP (headCPbis cp) interp = headCP (interp_CP cp interp).
proof: Proof. induction m. unfold interp_CP; unfold nat_rect; simpl; reflexivity. induction m; unfold interp_CP; unfold nat_rect; simpl; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets