In http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Finite.htmlthe collection of finite subsets Fin(A) of a set A is defined. I want to define a function
F : Fin(A) => A.What is the best way to go about this? None of my attempts parse. I realize that Fin(A) is not a type, but am not sure how to work around this.