proposition: Lemma cc_cast : forall f n (ls : Tes n) p (h : n=p) E v V, cc f (Vcast ls h) E v V <-> cc f ls E v V.
proof: Proof. intros f n ls p h E v V. subst p. rewrite Vcast_refl. refl. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)