proposition: Lemma obstring_ienc n s (H : |s| <= n) : ienc s = obcast H.
proof: Proof. unfold ienc. cbn. setoid_rewrite obstring_iprep. f_equal. apply bstring_eq, app_nil_r. Unshelve. rewrite app_length. cbn. 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