proposition: Lemma SN_terminates_step' t : Acc (fun x y => step y x) t -> terminates step' t.
proof: Proof. elim=> {}t _ IH. case: (step'_dec t). - move=> [t'] /[dup] H /step'_step /IH [?] [??]. eexists. split; [|eassumption]. apply: rt_trans; [apply: rt_step|]; eassumption. - move=> H. exists t. split; [apply: rt_refl|]. move=> ??. apply: H. eexists. eassumption. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect