proposition: Lemma step'_step_SN t : clos_refl_trans _ step' t I -> Acc (fun x y => step y x) t.
proof: Proof. move E: (I) => t' /clos_rt_rt1n_iff H. elim: H E. - move=> ? <-. constructor. move=> ?. move E: (I) => ? H. exfalso. case: H E=> //. by move=> > []. - move=> > /step'_step_det H _ IH ?. subst. constructor. move=> ? /H <-. by apply: IH. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect