FinSet =  Main +


consts Fin :: 'a set => 'a set set                   

inductive "Fin(A)"
  intrs
    emptyI  "{} : Fin(A)"
    insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)"


end