HomeIsabelle/Phabricator

Add well-foundedness of trivial unit relation