fact: Fixpoint enc_eterm (P : eterm) := match P with | closure Ps M => lam (call [var 1; enc_list enc_eterm Ps; enc_term M]) end.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect