proposition: Lemma clos_refl_trans_transport {s s' t} : sync s s' -> clos_refl_trans _ step1 s t -> exists t', sync t t' /\ clos_refl_trans _ step2 s' t'.
proof: Proof. Proof using fstep. intros Hss' Hst. apply clos_rt_rt1n in Hst. revert s' Hss'. induction Hst as [|??? Hxy Hyz IH]. - intros s' ?. exists s'. now split; [|apply rt_refl]. - intros s' Hxs'. destruct (fstep Hxy Hxs') as [y' [Hs'y' Hyy']]. destruct (IH _ Hyy') as [t' [? Hy't']]. exists t'. split; [|eapply rt_trans; [apply clos_trans_clos_refl_trans|]]; eassumption. Qed.
imports: Relations Transitive_Closure