proposition: Lemma FS_rtc : forall us t, FS t us -> red R # t (last us t).
proof: Proof. induction us. simpl. intros. apply rt_refl. simpl FS. intuition. apply rt_trans with a. apply rt_step. hyp. simpl. destruct us. apply rt_refl. rewrite last_default with (d2:=a). apply IHus. hyp. discr. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)