proposition: Lemma red_last_string_g : red E # last_string (g t).
proof: Proof. rewrite <- last_string'_g. unfold last_string'. apply FS_rtc. apply (rewrites_correct h1'). Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)