Subset Coercions in Coq
scientific article