proposition: Lemma Fhd_red_mod : forall E R t u, hd_red_mod E R t u -> hd_red_mod (Frs E) (Frs R) (Ft t) (Ft u).
proof: Proof. intros. redtac. unfold hd_red_mod. exists (Ft t0). split. apply Fred_rtc. hyp. apply Fhd_red. subst. apply hd_red_rule. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)