fact: Definition enc_list {X : Type} (f : X -> term) := fix rec (l : list X) := match l with | nil => lam (lam (call [var 2])) | cons x l => lam (lam (call [var 1; f x; rec l])) end.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect