proposition: Lemma size_terms_cast : forall n (ts : terms n) m (h : n=m), size_terms (Vcast ts h) = size_terms ts.
proof: Proof. induction ts; intro m. destruct m; intro h. rewrite Vcast_refl. refl. discr. destruct m; intro h0. discr. rewrite Vcast_cons. simpl. rewrite IHts. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)