fact: Fixpoint enc_list (ns : list nat) : nat := match ns with | [] => 0 | n::ns => enc_pair n (enc_list ns) end.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun