proposition: Lemma fin_Set_bijg : forall m, (Fin m) -> FinSetList (natPrefix m).
proof: Proof. unfold FinSetList. induction m as [| m Hind]; unfold Fin; introv Hl; exrepnd; [destruct m; allsimpl; try contradiction |]. allsimpl. revert Hl0; cases_ifd Hd; introv Hxx; try contradiction. unfold lt in Hdt. apply le_lt_eq_dec in Hdt. dorn Hdt. - apply lt_S_n in Hdt. assert (Fin m ) as Hf by (exists m0; cases_if; auto; try contradiction). apply Hind in Hf. exrepnd. exists a. apply in_app_iff. left; auto. - exists m. apply in_app_iff. right; auto. simpl. auto. Defined.
imports: list