fact: Fixpoint enc_term (M : term) := match M with | var x => lam (lam (lam (call [var 3; enc_nat x]))) | app M N => lam (lam (lam (call [var 2; enc_term M; enc_term N]))) | lam M => lam (lam (lam (call [var 1; enc_term M]))) end.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect