proposition: Lemma terminating_Acc {s} : terminates step2 s -> Acc (fun y x => step2 x y) s.
proof: Proof. Proof using step2_det. intros [t [Hst%clos_rt_rt1n Ht]]. induction Hst as [|??? Hxy Hyz IH]; constructor. - now intros y ?%Ht. - intros y' Hxy'. rewrite <- (step2_det Hxy Hxy'). now apply IH. Qed.
imports: Relations Transitive_Closure