proposition: Lemma string_of_term_fill : forall t c, string_of_term (fill c t) = string_of_cont c ++ string_of_term t.
proof: Proof. induction c. refl. simpl. rewrite Vmap_first_cast. arity1 is_unary_sig. simpl. rewrite IHc. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)