fact: Definition enc_halt_cbn_varS := lam (lam (lam (lam ( call [var 3; I; lam (lam (call [var 4; var 7; var 1; lam (lam (lam (call [var 3; var 9]))); var 4])) ])))).
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect