proposition: Lemma R_inj n m (X Y : Fin.t m) : Fin.R n X = Fin.R n Y -> X = Y.
proof: Proof. elim: n. { done. } by move=> n IH /= /pos_nxt_inj /IH. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun