proposition: Lemma string_of_cont_cont : forall t, string_of_cont (cont t) = string_of_term t.
proof: Proof. apply term_ind_forall. refl. intros f t IH. rewrite string_of_term_fun1, cont_fun1. simpl. rewrite IH. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)