proposition: Lemma IB_enc rho u : eval rho (enc u) = Some u.
proof: Proof. unfold enc. rewrite <- (app_nil_r u) at 2. now apply IB_eval_Some. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.PCP.Reductions.PCPb_iff_dPCPb Undecidability(Shared.ListAutomation)