proposition: Lemma Fred_rtc : forall R t u, red R # t u -> red (Frs R) # (Ft t) (Ft u).
proof: Proof. induction 1; intros. apply rt_step. apply Fred. hyp. apply rt_refl. apply rt_trans with (Ft y); auto. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)