proposition: Lemma fin_Set_bijf : forall m, FinSetList (natPrefix m) -> (Fin m).
proof: Proof. unfold FinSetList. induction m as [| m Hind]; introv Hl; exrepnd;[allsimpl;contradiction |]. allsimpl. exrepnd. apply in_app_iff in Hl0. allsimpl. dorn Hl0;[|dorn Hl0];try(contradiction). - exrepnd. assert ({n : nat $ LIn n (natPrefix m)}) as Harg by eauto. apply Hind in Harg. exrepnd. allunfold Fin. destruct Harg as [marg MP]. exists marg. destruct (lt_dec marg m);[| contradiction]. cases_ifd Hd;[trivial|]. destruct Hdf. apply lt_S; trivial. - subst. exists a. cases_ifd Hd;[constructor|]. destruct Hdf. auto. Defined.
imports: list