fact: Fixpoint colon s u := match s with | var n => var n | lam _ => app u (Psi s) | app s t => match s with | var n => var n | app s1 s2 => (id colon) s (lam (app (ren S (cbv_cbn t)) (lam (app (app (var 1) (var 0)) (ren S (ren S u)))))) | lam _ => colon t (lam (app (app (ren S (Psi s)) (var 0)) (ren S u))) end 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)