proposition: Lemma cdrv_mon' n s t : @cdrv n (ienc s) (ienc t) -> @cdrv (S n) (ienc s) (ienc t).
proof: Proof. destruct (le_dec (|s|) n) as [H|H], (le_dec (|t|) n) as [H'|H']. - repeat unshelve setoid_rewrite obstring_ienc; trivial; lia. - setoid_rewrite (obstring_ienc H). setoid_rewrite (obstring_ienc' H'). cbn. tauto. - rewrite (obstring_ienc' H). cbn. tauto. - rewrite (obstring_ienc' H). cbn. tauto. 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