fact: Fixpoint enc_term (s: term) : nat := match s with | var n => enc_pair 0 n | lam s => enc_pair 1 (enc_term s) | app s t => enc_pair (2 + enc_term t) (enc_term s) 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