proposition: Lemma apps_cast : forall n (ts : Tes n) p (h : n=p) t, apps t (Vcast ts h) = apps t ts.
proof: Proof. induction ts; destruct p; simpl; intros e t. rewrite Vcast_refl. refl. discr. discr. rewrite Vcast_cons. apply IHts. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)