proposition: Lemma cdrv_mon n (s t : obstring n) : cdrv s t -> @cdrv (S n) (obembed s) (obembed t).
proof: Proof. now destruct s as [ [s HS]|], t as [ [t HT]|]. 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