proposition: Lemma test_coinc_ok_for_col : forall pa pb pc ss st interp, ss_ok_for_col ss interp -> st_ok_for_col st interp -> test_coinc_for_col ss st pa pb pc = true -> Col (interp pa) (interp pb) (interp pc).
proof: Proof. intros pa pb pc ss st interp HSS HST HTest. assert (HCol := @test_coinc_ok Tarski_is_a_Arity_for_col Tarski_is_a_Coinc_predicates_for_col Tarski_is_a_Coinc_theory_for_col ss st interp (pa, (pb, pc)) HSS HST HTest). simpl in HCol; auto. Qed.
imports: NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_col GeoCoq.Tactics.Coinc.CoincR