proposition: Lemma interp_CPOK {m : nat} : forall (cp : cartesianPower positive (S m)) (interp: positive -> COINCpoint), CPToList (interp_CP cp interp) = map interp (CPToList cp).
proof: Proof. induction m; intros cp interp. simpl. reflexivity. induction m; try (clear IHm0). simpl. reflexivity. rewrite CPToListOK. rewrite <- interp_CPHdOK. rewrite <- interp_CPTlOK. rewrite IHm. simpl. reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets