proposition: Lemma CoappDup : forall cp interp, ~ List.NoDup (CPToList cp) -> app coinc (interp_CP cp interp).
proof: Proof. intros cp interp H. apply CoappDupAux in H. destruct H as [e [l [m' [cp' [HPerm [Hfst Hsnd]]]]]]. assert (Hmn := Permutation.Permutation_length HPerm). apply Permutation.Permutation_map with positive COINCpoint interp (CPToList cp') (CPToList cp) in HPerm. do 2 (rewrite <- interp_CPOK in HPerm). do 2 (rewrite <- lengthOfCPToList in Hmn). do 3 (apply eq_add_S in Hmn). subst. apply PermCoincOK with (interp_CP cp' interp); try assumption; clear HPerm. apply app_2_n_app with (interp (headCP cp')) (interp (headCP (tailCP cp'))) (interp_CP (tailCP (tailCP cp')) interp). rewrite Hsnd. apply coinc_bd. rewrite <- interp_CPHdOK. reflexivity. rewrite <- interp_CPTlOK. rewrite <- interp_CPHdOK. reflexivity. do 2 (rewrite <- interp_CPTlOK). reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets