proposition: Lemma encodes_countersI (cs : Vector.t nat n) : encodes_counters cs (encode_counters cs).
proof: Proof. elim: cs; first by constructor. move=> [|c] m cs IH; by eauto using @Forall2 with counters nocore. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun