proposition: Lemma bound_cbv_cbn k t : bound k t -> bound k (cbv_cbn t).
proof: Proof. elim. - move=> *. do 3 constructor; lia. - move=> * /=. do 2 constructor. + by apply: bound_ren; [eassumption|lia]. + do 2 constructor. * rewrite !simpl_term /=. apply: bound_ren; [eassumption|lia]. * do 2 constructor; [constructor|]; constructor; lia. - move=> * /=. do 3 constructor; first by lia. apply: bound_ren; [eassumption|]. move=> [|n] /=; lia. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)