proposition: Theorem reduction : wCBNclosed ⪯ KrivineMclosed_HALT.
proof: Proof. exists id. move=> [s Hs]. have H's : closed s. { apply: closed_I => k. by rewrite L_subst_Lambda_subst. } split. - move=> [t]. move: H's => /Argument.simulation /[apply]. apply. by constructor. - move=> /Argument.inverse_simulation [t'] /=. rewrite Hs. move=> ?. by exists t'. Qed.
imports: Undecidability.LambdaCalculus(Lambda Krivine Util.term_facts Util.wCBN_facts Util.Krivine_facts) List Relations ssreflect Undecidability.Synthetic.Definitions