fact: Fixpoint enc_nat (n : nat) : term := match n with | 0 => lam (lam (call [var 2])) | S n => lam (lam (call [var 1; enc_nat n])) end.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect