proposition: Lemma string_of_term_fun1 : forall f t, string_of_term (Fun1 f t) = f :: string_of_term t.
proof: Proof. intros. unfold AUnary.Fun1. unfold string_of_term; fold string_of_term. rewrite Vmap_first_cast. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)