proposition: Lemma trs_of_srs_epi : forall R, (forall a, In a R -> maxvar (lhs a) = 0 /\ maxvar (rhs a) = 0) -> trs_of_srs (srs_of_trs R) = Fl HF R.
proof: Proof. induction R; intros. refl. simpl. rewrite IHR. assert (In a (a::R)). simpl. auto. destruct (H _ H0). rewrite rule_of_srule_epi; try hyp. refl. intros b h. assert (In b (a::R)). simpl. auto. destruct (H _ H0). intuition. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)