proposition: Lemma size_sub : forall t, size (sub s t) = size t.
proof: Proof. intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => size_terms (Vmap (sub s) ts) = size_terms ts); clear t. simpl. intro. destruct (hs x). rewrite H. refl. intros. rewrite sub_fun, !size_fun, H. refl. refl. intros. simpl. rewrite H, H0. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)