proposition: Lemma red_last_term_g : red E # last_term (g t).
proof: Proof. rewrite <- last_term'_g. unfold last_term'. apply FS_rtc. apply (rewrites_correct h1'). Qed.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)