proposition: Lemma reducts_vec_cast : forall f ts k (us : terms k) h k' (e : k = k') h', reducts_vec f ts (Vcast us e) h' = reducts_vec f ts us h.
proof: Proof. induction us; intros; destruct k'; try discr. rewrite Vcast_refl. refl. rewrite Vcast_cons. simpl. inversion e. subst k'. apply app_eq. apply map_eq. intros. apply args_eq. apply Vreplace_pi. lia. apply IHus. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)