proposition: Lemma HF : forall f, arity f = arity (F f).
proof: Proof. intro. rewrite <- is_unary_sig. refl. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)