proposition: Theorem reduction : HaltLclosed ⪯ wCBNclosed.
proof: Proof. exists (fun '(exist _ s Hs) => exist _ (Argument.colon s (lam (var 0))) (Argument.closed_colon Hs)). move=> [s Hs]. split. - move=> [t] /= /[dup] [[_ []]] t' ->. move=> /eval_iff /= /Argument.simulation. move=> /(_ Hs (lam (var 0))) ?. exists (Argument.cbv_cbn t'). apply: rt_trans; first by eassumption. apply: rt_step. by apply: wCBN_stepSubst. - move=> [t] /Argument.inverse_simulation. by apply. 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) Undecidability.Synthetic.Definitions