proposition: Lemma obstring_ienc' n s (H : ~ |s| <= n) : @ienc _ (FIB n) s = None.
proof: Proof. induction s; cbn in *; try lia. change (@ccons n a (ienc s) = None). destruct (le_dec (|s|) n) as [H'|H']. - setoid_rewrite (obstring_ienc H'). cbn. destruct le_dec; tauto. - now rewrite IHs. 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