proposition: Lemma noConf_fin_hom_equiv : forall n, NoConfusionPackage (fin n).
proof: Proof. unshelve econstructor. refine noConf_fin. apply noConf_fin_eq. apply noConf_fin_eq_inv. apply noConf_fin_eq_eq_inv. Defined.
imports: Equations(Equations DepElimDec HSets) Utf8