proposition: Lemma rewt_count x : rewt G [S] x -> count x S <= 1.
proof: Proof. induction 1. - cbn. now rewrite Nat.eqb_refl. - inversion H0. subst. clear H0. destruct H1 as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inversion H0; subst. + eauto. + unfold Sigma. simpl_list. rewrite <- !countSplit in *. cbn in *. rewrite Nat.eqb_refl in *. enough (count l S = 0) as ->. { enough (count l0 S = 0) as ->. { lia. } eapply notInZero. intros D. edestruct (fresh_spec) with (l := Sigma); try reflexivity. eapply sym_word_R in H1. unfold Sigma. eauto. } eapply notInZero. intros D. edestruct (fresh_spec) with (l := Sigma); try reflexivity. eapply sym_word_l in H1. unfold Sigma. eauto. + unfold Sigma. simpl_list. rewrite <- !countSplit in *. cbn in *. rewrite Nat.eqb_refl in *. assert (S =? a = false) as ->. { eapply Nat.eqb_neq. intros D. edestruct fresh_spec with (l := Sigma); try reflexivity. unfold S in *. rewrite D. unfold Sigma; eauto. } enough (count l S = 0) as ->. { enough (count l0 S = 0) as ->. { lia. } eapply notInZero. intros D. edestruct (fresh_spec) with (l := Sigma); try reflexivity. eapply sym_word_R in H1. unfold Sigma. eauto. } eapply notInZero. intros D. edestruct (fresh_spec) with (l := Sigma); try reflexivity. eapply sym_word_l in H1. unfold Sigma. eauto. Qed.
imports: Setoid Morphisms List Arith Lia Undecidability.CFG.CFP Undecidability.CFG.CFG Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions