proposition: Lemma mk_call_cast : forall f n (ts : Tes n) p (h : n=p), mk_call f (Vcast ts h) = mk_call f ts.
proof: Proof. intros f n ts p h. subst p. rewrite Vcast_refl. refl. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)