proposition: Lemma drv_cdrv s t : derivable R s t <-> @cdrv (max (|s|) (|t|)) (ienc s) (ienc t).
proof: Proof. repeat unshelve setoid_rewrite obstring_ienc; try reflexivity; 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