proposition: Lemma collect_coincs_for_col : forall A B C pa pb pc ss interp, Col A B C -> interp pa = A -> interp pb = B -> interp pc = C -> ss_ok_for_col ss interp -> ss_ok_for_col (SS.add (@CPToSS 3 (pa, (pb, pc))) ss) interp.
proof: Proof. intros A B C pa pb pc ss interp HCol HA HB HC HSS. apply (@collect_coincs Tarski_is_a_Arity_for_col Tarski_is_a_Coinc_predicates_for_col); [apply Tarski_is_a_Coinc_theory_for_col|simpl|auto]. rewrite HA; rewrite HB; rewrite HC; auto. Qed.
imports: NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_col GeoCoq.Tactics.Coinc.CoincR