proposition: Lemma rule_of_srule_epi : forall a, maxvar (lhs a) = 0 -> maxvar (rhs a) = 0 -> rule_of_srule (srule_of_rule a) = Fr HF a.
proof: Proof. intros [l r] hl hr. unfold rule_of_srule, srule_of_rule. simpl. rewrite !term_of_string_epi; try hyp. refl. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)