proposition: Lemma collect_wds_for_col : forall A B pa pb st interp, A <> B -> interp pa = A -> interp pb = B -> st_ok_for_col st interp -> st_ok_for_col (STadd (pa, pb) st) interp.
proof: Proof. intros A B pa pb st interp HDiff HA HB HST. apply (@collect_wds 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; auto. Qed.
imports: NArith GeoCoq.Utils.sets GeoCoq.Meta_theory.Models.tarski_to_coinc_theory_for_col GeoCoq.Tactics.Coinc.CoincR