fact: Definition Psi (t : term) := match t with | var n => var n | app s t => app s t | lam s => lam (cbv_cbn s) end.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)