proposition: Lemma string_of_term_reset : forall t, string_of_term (reset t) = string_of_term t.
proof: Proof. intro t; pattern t; apply term_ind_forall; clear t; intros; unfold reset. simpl. unfold swap, single. rewrite (beq_refl beq_nat_ok). refl. rewrite sub_fun1, !string_of_term_fun1, var_fun1. fold (reset t). rewrite H. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)