proposition: Lemma test_coinc_ok : forall ss st interp cp, ss_ok ss interp -> st_ok st interp -> test_coinc ss st cp = true -> app coinc (interp_CP cp interp).
proof: Proof. intros ss st interp cp HSS HST HTC. unfold test_coinc in *. assert (HSS2 : ss_ok (identify_varieties ss st) interp) by (apply identify_varieties_ok; assumption). unfold ss_ok in HSS2. apply SSWEqP.MP.Dec.F.exists_2 in HTC. unfold SS.Exists in HTC. destruct HTC as [s [HIn Hmem]]. apply HSS2 with s. apply SSWEqP.MP.Dec.F.mem_1. assumption. assumption. intros x y Hxy. apply memCPProper; trivial. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets