proposition: Lemma reducts_vec_pi : forall f ts k (us : terms k) h h', reducts_vec f ts us h = reducts_vec f ts us h'.
proof: Proof. intros. assert (h=h'). apply le_unique. subst h'. refl. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)