For refine def obligations involving functions, use exensionality to get more convenient and readable equalities
For refine def obligations involving functions, use exensionality to
get more convenient and readable equalities


git-svn-id: 9ecf60ce9baff443e30a0472d3fd222fcb8117cf@7265 7b97033b-253e-4a5c-9b07-e25f9089a9fd

KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware