proposition: Lemma fin_Set : bijection (fin_Set_bijf 3) (fin_Set_bijg 3).
proof: Proof. unfolds_base. unfold Fin; dands; unfolds_base; intro s. - unfold FinSetList in s. simpl in s. exrepnd. repeat(in_reasoning); try contradiction; subst; simpl; refl. - simpl in s. exrepnd. revert s0. destruct m;[|destruct m]. + simpl. intro; destruct s0; auto. + simpl. intro; destruct s0; auto. + simpl. destruct m. * intro; destruct s0; auto. * intro. simpl in s0. inverts s0. Qed.
imports: list