proposition: Lemma terminates_transport {s s'} : sync s s' -> terminates step1 s -> terminates step2 s'.
proof: Proof. Proof using fstop fstep. intros Hss' [t [Hst Ht]]. destruct (clos_refl_trans_transport Hss' Hst) as [t' [Htt' Hs't']]. apply (terminates_extend _ Hs't'). eapply fstop; eassumption. Qed.
imports: Relations Transitive_Closure