proposition: Lemma obstring_iprep n x u (HX : |x++u| <= n) (HU : |u| <= n) : iprep x (obcast HU) = obcast HX.
proof: Proof. induction x; cbn. - f_equal. now apply bstring_eq. - assert (H : |x++u| <= n). { rewrite app_length in *. cbn in HX. lia. } rewrite (IHx H). unfold ccons, bcast at 1. destruct le_dec. + f_equal. now apply bstring_eq. + exfalso. cbn in *. rewrite app_length in *. lia. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation