fact: Definition ss_ok_for_col ss interp := @ss_ok Tarski_is_a_Arity_for_col Tarski_is_a_Coinc_predicates_for_col ss interp.
imports: NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_col GeoCoq.Tactics.Coinc.CoincR