proposition: Lemma Fred : forall R t u, red R t u -> red (Frs R) (Ft t) (Ft u).
proof: Proof. intros. redtac. unfold red. subst. exists (Ft l). exists (Ft r). exists (Fc c). exists (Fs s). intuition. change (Frs R (Fr (mkRule l r))). exists (mkRule l r). intuition. rewrite Ft_fill, Ft_sub. refl. rewrite Ft_fill, Ft_sub. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)