proposition: Lemma noConfVec_hom_equiv : forall {E A : Set} n, NoConfusionPackage (Vec E A n).
proof: Proof. unshelve econstructor. refine noConfVec. apply noConfVec_eq. apply noConfVec_eq_inv. apply noConfVec_eq_eq_inv. Defined.
imports: Equations(Equations DepElimDec HSets) Utf8