proposition: Lemma bound_colon {n s u} : bound n s -> bound n u -> bound n (colon s u).
proof: Proof. move=> H. elim: H u. - move=> * /=. by constructor. - move=> ? [?|??|?] ? IH'1 IH1 ? IH2 ??. + done. + move=> /=. apply: IH1. do 2 constructor. * apply: bound_ren; [apply: bound_cbv_cbn; eassumption|lia]. * do 2 constructor; [do 2 constructor|]; [lia ..|]. rewrite simpl_term /=. apply: bound_ren; [eassumption|lia]. + move=> /=. apply: IH2. do 2 constructor. * do 2 constructor; [|lia]. move=> /boundE in IH'1. apply: bound_ren; [apply: bound_cbv_cbn; eassumption|]. move=> [|?] /=; lia. * apply: bound_ren; [eassumption|lia]. - move=> * /=. constructor; [done|constructor]. by apply: bound_cbv_cbn. 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)